Skip to content
Browse files

Repair the configure after Hugo's last "repair" ;-)

 Ok, I wasn't aware of the funny behavior of cd in presence of $CDPATH.
 But the last "repair" was worse, trying to write into non-existing file
 theories/config/coq_config.ml

 Things should be better now:

 * no more Coq_config.theories_dirs at all, since it was completely unused :-)

 * concerning Coq_config.plugins_dirs, we list them without any "cd" into plugins,
   hence keeping the "plugins/" part in their paths, and adapt accordingly
   the only use (!) of plugins_dirs, in coq_makefile

 Please run ./configure again after upgrading to this commit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15860 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
1 parent 985580c commit 87b9f636f602e6067314ac994777e54307a72a65 letouzey committed Oct 5, 2012
Showing with 2 additions and 13 deletions.
  1. +0 −1 config/coq_config.mli
  2. +1 −11 configure
  3. +1 −1 tools/coq_makefile.ml
View
1 config/coq_config.mli
@@ -49,7 +49,6 @@ val compile_date : string (* compile date *)
val vo_magic_number : int
val state_magic_number : int
-val theories_dirs : string list
val plugins_dirs : string list
val exec_extension : string (* "" under Unix, ".exe" under MS-windows *)
View
12 configure
@@ -1030,18 +1030,8 @@ let localwwwrefman = "file:/" ^ docdir ^ "html/refman"
END_OF_COQ_CONFIG
-# Subdirectories of theories/ added in coq_config.ml
-# Note: don't propagate output of cd if any: it's verbose when CDPATH is defined
-subdirs () {
- (cd $1; find * \( -name .svn -prune \) -o \( -type d -exec printf "\"%s\";\n" {} \; \) >> "$mlconfig_file")
-}
-
-echo "let theories_dirs = [" >> "$mlconfig_file"
-subdirs theories
-echo "]" >> "$mlconfig_file"
-
echo "let plugins_dirs = [" >> "$mlconfig_file"
-subdirs plugins
+find plugins/* \( -name .svn -prune \) -o \( -type d -exec printf "\"%s\";\n" {} \; \) >> "$mlconfig_file"
echo "]" >> "$mlconfig_file"
chmod a-w "$mlconfig_file"
View
2 tools/coq_makefile.ml
@@ -408,7 +408,7 @@ let variables is_install opt (args,defs) =
-I $(COQLIB)proofs -I $(COQLIB)tactics -I $(COQLIB)tools \\
-I $(COQLIB)toplevel -I $(COQLIB)grammar";
List.iter (fun c -> print " \\
- -I $(COQLIB)plugins/"; print c) Coq_config.plugins_dirs; print "\n";
+ -I $(COQLIB)/"; print c) Coq_config.plugins_dirs; print "\n";
print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n";
print "CAMLC?=$(OCAMLC) -c -rectypes\n";
print "CAMLOPTC?=$(OCAMLOPT) -c -rectypes\n";

0 comments on commit 87b9f63

Please sign in to comment.
Something went wrong with that request. Please try again.