diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-18 20:56:21 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-18 20:56:21 +0000 |
| commit | 85237f65161cb9cd10119197c65c84f65f0262ee (patch) | |
| tree | 263ba9669e047ea32cf6734a878d747e26c7f2be /lib/envars.ml | |
| parent | 05b31844f683c3bc81b371c94be5cc6f6f4edf61 (diff) | |
Backporting from v8.2 to trunk:
- Filtering of doc compilation messages (11793,11795,11796).
- Fixing bug #1925 and cleaning around bug #1894 (11796, 11801).
- Adding some tests.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11802 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/envars.ml')
| -rw-r--r-- | lib/envars.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/lib/envars.ml b/lib/envars.ml index 867297a86..3246c1478 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -20,14 +20,13 @@ let guess_coqlib () = then Coq_config.coqlib else let prefix = Filename.dirname (Filename.dirname Sys.executable_name) in - let coqlib = if Coq_config.local then prefix else + let coqlib = if !Flags.boot || Coq_config.local then prefix else List.fold_left Filename.concat prefix ["lib";"coq"] 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" let coqlib () = - if !Flags.coqlib_spec then !Flags.coqlib else - (if !Flags.boot then Coq_config.coqsrc else guess_coqlib ()) + if !Flags.coqlib_spec then !Flags.coqlib else guess_coqlib () let path_to_list p = let sep = if Sys.os_type = "Win32" then ';' else ':' in |