Skip to content

Commit 97365a4

Browse files
committed
OPAM: remove manual install and use Makefile
1 parent e4211e1 commit 97365a4

File tree

2 files changed

+2
-10
lines changed

2 files changed

+2
-10
lines changed

coq-vst-32.opam

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -19,11 +19,7 @@ license: "https://raw.githubusercontent.com/PrincetonUniversity/VST/master/LICEN
1919
build: [make "BITSIZE=32" "-j%{jobs}%" "msl" "sepcomp" "veric" "floyd"]
2020
run-test: [make "BITSIZE=32" "-j%{jobs}%" "progs" "sha-hmac" "mailbox"]
2121
install: [
22-
["mkdir" "-p" "%{lib}%/coq/user-contrib/VST"]
23-
["cp" "-r" "msl" "%{lib}%/coq/user-contrib/VST/"]
24-
["cp" "-r" "veric" "%{lib}%/coq/user-contrib/VST/"]
25-
["cp" "-r" "floyd" "%{lib}%/coq/user-contrib/VST/"]
26-
["cp" "-r" "sepcomp" "%{lib}%/coq/user-contrib/VST/"]
22+
make "BITSIZE=32" "install"
2723
]
2824
depends: [
2925
"coq" {>= "8.11.0"}

coq-vst.opam

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -19,11 +19,7 @@ license: "https://raw.githubusercontent.com/PrincetonUniversity/VST/master/LICEN
1919
build: [make "BITSIZE=64" "-j%{jobs}%" "msl" "sepcomp" "veric" "floyd"]
2020
run-test: [make "BITSIZE=64" "-j%{jobs}%" "progs"]
2121
install: [
22-
["mkdir" "-p" "%{lib}%/coq/user-contrib/VST"]
23-
["cp" "-r" "msl" "%{lib}%/coq/user-contrib/VST/"]
24-
["cp" "-r" "veric" "%{lib}%/coq/user-contrib/VST/"]
25-
["cp" "-r" "floyd" "%{lib}%/coq/user-contrib/VST/"]
26-
["cp" "-r" "sepcomp" "%{lib}%/coq/user-contrib/VST/"]
22+
make "BITSIZE=64" "install"
2723
]
2824
depends: [
2925
"coq" {>= "8.11.0"}

0 commit comments

Comments
 (0)