coq-makefile: strip windows drive letter when DESTDIR is not empty

In unix one can concatenate a prefix with an absolute path in
order to obtain a valid path.  This is not the case on Windows.

2 files changed, 30 insertions, 21 deletions

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 841ee45711..f1e519d038 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -184,10 +184,6 @@ endif
 
 PP:=-pp '$(CAMLP4O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" compat5.cmo $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'
 
-COQLIBINSTALL = $(COQLIB)user-contrib
-COQDOCINSTALL = $(DOCDIR)user-contrib
-COQTOPINSTALL = $(COQLIB)toploop
-
 ifneq (,$(TIMING))
 TIMING_ARG=-time
 ifeq (after,$(TIMING))
@@ -208,6 +204,12 @@ ifneq "$(DSTROOT)" ""
 DESTDIR := $(DSTROOT)
 endif
 
+concat_path = $(if $(1),$(1)/$(subst $(COQMF_WINDRIVE),/,$(2)),$(2))
+
+COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)user-contrib)
+COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)user-contrib)
+COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)toploop)
+
 # Files #######################################################################
 #
 # We here define a bunch of variables about the files being part of the
@@ -444,9 +446,9 @@ install: install-extra
 	 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" &&\
-	   echo INSTALL "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df";\
+	   install -d "$(COQLIBINSTALL)/$$df" &&\
+	   install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\
+	   echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\
 	 fi;\
 	done
 install-extra::
@@ -459,24 +461,24 @@ install-byte:
 	 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" &&\
-	   echo INSTALL "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df";\
+	   install -d "$(COQLIBINSTALL)/$$df" &&\
+	   install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\
+	   echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\
 	 fi;\
 	done
 
 install-doc:: html mlihtml
 	@# Extension point
-	$(HIDE)install -d "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html"
+	$(HIDE)install -d "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html"
 	$(HIDE)for i in html/*; do \
-	 dest="$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\
+	 dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\
 	 install -m 0644 "$$i" "$$dest";\
 	 echo INSTALL "$$i" "$$dest";\
 	done
 	$(HIDE)install -d \
-		"$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml"
+		"$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml"
 	$(HIDE)for i in mlihtml/*; do \
-	 dest="$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\
+	 dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\
 	 install -m 0644 "$$i" "$$dest";\
 	 echo INSTALL "$$i" "$$dest";\
 	done
@@ -486,20 +488,20 @@ uninstall::
 	@# Extension point
 	$(HIDE)for f in $(FILESTOINSTALL); do \
 	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\
-	 instf="$(DESTDIR)$(COQLIBINSTALL)/$$df/`basename $$f`" &&\
+	 instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\
 	 rm -f "$$instf" &&\
 	 echo RM "$$instf" &&\
-	 (rmdir "$(DESTDIR)$(COQLIBINSTALL)/$$df/" || true); \
+	 (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" || true); \
 	done
 .PHONY: uninstall
 
 uninstall-doc::
 	@# Extension point
-	$(SHOW)'RM $(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html'
-	$(HIDE)rm -rf "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html"
-	$(SHOW)'RM $(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml'
-	$(HIDE)rm -rf "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml"
-	$(HIDE) rmdir "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true
+	$(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html'
+	$(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html"
+	$(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml'
+	$(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml"
+	$(HIDE) rmdir "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true
 .PHONY: uninstall-doc
 
 # Cleaning ####################################################################
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 0e0375c008..327f53520c 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -193,12 +193,19 @@ let generate_conf_includes oc { ml_includes; r_includes; q_includes } =
     (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes))
 ;;
 
+let windrive s =
+  if Coq_config.arch_is_win32 && Str.(string_match (regexp "^[a-zA-Z]:") s 0)
+  then Str.matched_string s
+  else s
+;;
+
 let generate_conf_coq_config oc args bypass_API =
   section oc "Coq configuration.";
   let src_dirs = if 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_WINDRIVE=%s\n" (windrive Coq_config.coqlib)
 ;;
 
 let generate_conf_files oc