diff options
| -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 478ae4374e..2eede84937 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"; |