aboutsummaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorChantal Keller <Chantal.Keller@lri.fr>2017-10-03 11:03:44 +0200
committerChantal Keller <Chantal.Keller@lri.fr>2017-10-03 11:03:44 +0200
commitca5213e2a653640cab6d98c1b0e799262b6be33d (patch)
treea2823893e4f7ab9ccfe6c62b5c4b03ac1a7a7c75 /src
parent1cedf0df745cc5ed6bf5031b59f84fc37c8ce9f0 (diff)
downloadsmtcoq-ca5213e2a653640cab6d98c1b0e799262b6be33d.tar.gz
smtcoq-ca5213e2a653640cab6d98c1b0e799262b6be33d.zip
make install for Coq-8.6
Diffstat (limited to 'src')
-rw-r--r--src/versions/standard/Make11
-rw-r--r--src/versions/standard/Makefile3
2 files changed, 4 insertions, 10 deletions
diff --git a/src/versions/standard/Make b/src/versions/standard/Make
index 2445f87..1cfad12 100644
--- a/src/versions/standard/Make
+++ b/src/versions/standard/Make
@@ -12,14 +12,9 @@
## Suppress the "Makefile" target ##
## Suppress the "test", "ztest", "vtest" and "./" dependencies from ##
## the all target ##
-
-## Change the "all" target into: ##
-## all: ml $(CMXFILES) $(CMXA) $(CMXS) $(VOFILES) ##
-## Change the "install-natdynlink" target: change CMXSFILES into CMXS and add the same thing for CMXA. ##
-## Change the "install" target: change CMO into CMX. ##
-## Remove the automatically generated line with %.cmxs: %.cmx ##
-## Finally, suppress the "Makefile" target and add to the "clean" target: ##
-## - rm -f ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.mli smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtcoq.a ##
+## Suppress the "+" lines of the install and the clean targets ##
+## Add to the clean target: ##
+## - rm -f ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.mli smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml ##
########################################################################
diff --git a/src/versions/standard/Makefile b/src/versions/standard/Makefile
index 1a6eb97..a90104c 100644
--- a/src/versions/standard/Makefile
+++ b/src/versions/standard/Makefile
@@ -437,7 +437,6 @@ install:$(if $(HASNATDYNLINK_OR_EMPTY),install-natdynlink)
install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i`"; \
install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i; \
done
- +cd ./ && $(MAKE) DSTROOT="$(DSTROOT)" INSTALLDEFAULTROOT="$(INSTALLDEFAULTROOT)/./" install
install-doc:
install -d "$(DSTROOT)"$(COQDOCINSTALL)/SMTCoq/html
@@ -521,7 +520,7 @@ clean::
- rm -rf test
- rm -rf ztest
- rm -rf vtest
- +cd ./ && $(MAKE) clean
+ - rm -f ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.mli smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml
cleanall:: clean
rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux)