From 87b9f636f602e6067314ac994777e54307a72a65 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 5 Oct 2012 13:35:43 +0000 Subject: 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 --- config/coq_config.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'config') diff --git a/config/coq_config.mli b/config/coq_config.mli index 2f8ea5a41..f2861f12a 100644 --- a/config/coq_config.mli +++ b/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 *) -- cgit v1.2.3