aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authornotin2009-02-11 14:39:19 +0000
committernotin2009-02-11 14:39:19 +0000
commitfe0e355164bf8401ee5f2397584d3e3a04b82240 (patch)
tree34cf1b61daf7b26ad8cd9c23447e4c5ce07775e3 /lib
parentc3acdf3caca52e3b09ac075f043c4eddfe5d0814 (diff)
Gestion des espaces dans les noms + guess_coqlib sous Windows
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11921 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
-rw-r--r--lib/envars.ml5
1 files changed, 3 insertions, 2 deletions
diff --git a/lib/envars.ml b/lib/envars.ml
index 5887adcdeb..d700ffe160 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -21,8 +21,9 @@ let guess_coqlib () =
else
let coqbin = System.canonical_path_name (Filename.dirname Sys.executable_name) in
let prefix = Filename.dirname coqbin in
- let coqlib = if Coq_config.local then prefix else
- List.fold_left Filename.concat prefix ["lib";"coq"] in
+ let rpath = if Coq_config.local then [] else
+ (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) in
+ let coqlib = List.fold_left Filename.concat prefix rpath in
if Sys.file_exists (Filename.concat coqlib file) then coqlib else
Util.error "cannot guess a path for Coq libraries; please use -coqlib option"