diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-19 14:47:23 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-19 14:47:23 +0000 |
| commit | 736ffcea3a04da40ea3047216864ca420f220fe5 (patch) | |
| tree | 84f14a48b0071aaae5616e8b8f1efc382e294f91 | |
| parent | 826eb7c6d11007dfd747d49852e71a22e0a3850a (diff) | |
Made the filename of compiled files explicit, i.e. add a ./ prefix
whenever the filename was given alone. This caused strange behaviour
of coqtop that was compiling stuff we didn't want to just because
it was somewhere in its loadpath.
This is why FingerTree was not compiling, btw, as it had two files
equally named in two different paths.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16788 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/coqtop.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 79467cacd..ed5e92867 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -120,6 +120,13 @@ let add_compile verbose s = set_batch_mode (); Flags.make_silent true; if not !glob_opt then Dumpglob.dump_to_dotglob (); + (** make the file name explicit; needed not to break up Coq loadpath stuff. *) + let s = + let open Filename in + if is_implicit s + then concat current_dir_name s + else s + in compile_list := (verbose,s) :: !compile_list let compile_file (v,f) = |