diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-10-06 08:53:23 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-10-06 08:53:23 +0200 |
| commit | b770451a4b3c74db78457951f75505b53d362c12 (patch) | |
| tree | 162199758b76f573db9b4da5d73b9df440c58ab9 | |
| parent | 6adbf7d9678257aa42ef0d3b30db2e484cd148ad (diff) | |
fix wrong escaping in coq_makefile
| -rw-r--r-- | tools/coq_makefile.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 478ae4374..2eede8493 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -195,7 +195,7 @@ let install_include_by_root = print "\tfor i in "; print_list " " (List.rev_map (Format.sprintf "$(%sINC)") l); print "; do \\\n"; - printf "\t if [ $${$$i%%%%top.cmxs} = $$i ]; then\\\n"; + printf "\t if [ $${i%%%%top.cmxs} = $$i ]; then\\\n"; printf "\t install -m 0644 $$i \"$(DSTROOT)\"$(COQLIBINSTALL)/%s/`basename $$i`; \\\n" d; printf "\t else \\\n"; printf "\t install -m 0644 $$i \"$(DSTROOT)\"$(COQTOPINSTALL)/`basename $$i`; \\\n"; |