diff options
| author | notin | 2009-02-11 14:39:19 +0000 |
|---|---|---|
| committer | notin | 2009-02-11 14:39:19 +0000 |
| commit | fe0e355164bf8401ee5f2397584d3e3a04b82240 (patch) | |
| tree | 34cf1b61daf7b26ad8cd9c23447e4c5ce07775e3 /lib | |
| parent | c3acdf3caca52e3b09ac075f043c4eddfe5d0814 (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.ml | 5 |
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" |
