coq_makefile: explicit target install-toploop for toploop plugins

1 files changed, 7 insertions, 5 deletions

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 2eede8493..0afafff6e 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -195,11 +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  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";
-      printf "\t fi\\\n";
+      printf "\t install -m 0644 $$i \"$(DSTROOT)\"$(COQLIBINSTALL)/%s/`basename $$i`; \\\n" d;
       printf "\tdone\n"
   in function
   |None,l -> List.iter (install_dir (fun _ _ -> ())) l
@@ -273,6 +269,12 @@ let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) in
       install_include_by_root where_what_cmxs;
       print "\n";
     end;
+    if (not_empty cmxsfiles) then begin
+      print "install-toploop: $(MLLIBFILES:.mllib=.cmxs)\n";
+      printf "\t install -d \"$(DSTROOT)\"$(COQTOPINSTALL)/\n";
+      printf "\t install -m 0644 $?  \"$(DSTROOT)\"$(COQTOPINSTALL)/\n";
+      print "\n";
+    end;
     print "install:";
     if (not_empty cmxsfiles) then print "$(if $(HASNATDYNLINK_OR_EMPTY),install-natdynlink)";
     print "\n";