diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-07-17 15:02:47 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-07-20 15:43:04 +0200 |
| commit | 1fd1ca0703811392c890c41a796ed7efdaacca28 (patch) | |
| tree | 37e900096db2ab13c57987a170bd0db3e5427b8f | |
| parent | 82b197a87e154d5206d74dfe53f5b5f5215f1a3e (diff) | |
coq-makefile: treat coq_makefile as any other coq binary
In particular, find it under $(COQBIN)
| -rw-r--r-- | tools/CoqMakefile.in | 29 | ||||
| -rw-r--r-- | tools/coq_makefile.ml | 1 |
2 files changed, 16 insertions, 14 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 7d281977a..841ee4571 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -87,6 +87,9 @@ COQDEP ?= "$(COQBIN)coqdep" GALLINA ?= "$(COQBIN)gallina" COQDOC ?= "$(COQBIN)coqdoc" COQMKTOP ?= "$(COQBIN)coqmktop" +COQMKFILE ?= "$(COQBIN)coq_makefile" + +# Timing scripts COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py" COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py" COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py" @@ -437,12 +440,12 @@ beautify: $(BEAUTYFILES) install: install-extra $(HIDE)for f in $(FILESTOINSTALL); do\ - df="`$(COQMF_MAKEFILE) -destination-of "$$f" $(COQLIBS)`";\ - if [ -z "$$df" ]; then\ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ + if [ "$$?" != "0" -o -z "$$df" ]; then\ echo SKIP "$$f" since it has no logical path;\ else\ - install -d "$(DESTDIR)$(COQLIBINSTALL)/$$df"; \ - install -m 0644 "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df"; \ + install -d "$(DESTDIR)$(COQLIBINSTALL)/$$df" &&\ + install -m 0644 "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df" &&\ echo INSTALL "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df";\ fi;\ done @@ -452,12 +455,12 @@ install-extra:: install-byte: $(HIDE)for f in $(BYTEFILESTOINSTALL); do\ - df="`$(COQMF_MAKEFILE) -destination-of "$$f" $(COQLIBS)`";\ - if [ -z "$$df" ]; then\ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ + if [ "$$?" != "0" -o -z "$$df" ]; then\ echo SKIP "$$f" since it has no logical path;\ else\ - install -d "$(DESTDIR)$(COQLIBINSTALL)/$$df"; \ - install -m 0644 "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df"; \ + install -d "$(DESTDIR)$(COQLIBINSTALL)/$$df" &&\ + install -m 0644 "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df" &&\ echo INSTALL "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df";\ fi;\ done @@ -482,11 +485,11 @@ install-doc:: html mlihtml uninstall:: @# Extension point $(HIDE)for f in $(FILESTOINSTALL); do \ - df="`$(COQMF_MAKEFILE) -destination-of "$$f" $(COQLIBS)`";\ - instf="$(DESTDIR)$(COQLIBINSTALL)/$$df/`basename $$f`"; \ - rm -f "$$instf";\ - echo RM "$$instf"; \ - rmdir "$(DESTDIR)$(COQLIBINSTALL)/$$df/" || true; \ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ + instf="$(DESTDIR)$(COQLIBINSTALL)/$$df/`basename $$f`" &&\ + rm -f "$$instf" &&\ + echo RM "$$instf" &&\ + (rmdir "$(DESTDIR)$(COQLIBINSTALL)/$$df/" || true); \ done .PHONY: uninstall diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index c76b68dab..0e0375c00 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -199,7 +199,6 @@ let generate_conf_coq_config oc args bypass_API = then Coq_config.all_src_dirs else Coq_config.api_dirs @ Coq_config.plugins_dirs @ ["-open API"] in Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs; - fprintf oc "COQMF_MAKEFILE=%s\n" (quote (List.hd args)); ;; let generate_conf_files oc |