diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-15 11:54:45 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-10-06 17:21:46 +0200 |
| commit | b0b9ec7c16c38dabc7c4279dbe4d578b74e91c19 (patch) | |
| tree | 2dbacaa7d6e91c61f29946f38befc05e310d1a59 /toplevel/coqinit.ml | |
| parent | f1598b00219a951e94036cb7f48a8fe1309025f1 (diff) | |
[coqtop] Don't reset coqinit internal variables after initialization.
We remove `init_library_roots` as there is no point in resetting this
internal variable. Its only user is `init_load_path` and this function
is not meant (and is not) idempotent now.
Diffstat (limited to 'toplevel/coqinit.ml')
| -rw-r--r-- | toplevel/coqinit.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 5ca886965..1d5406770 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -114,9 +114,6 @@ let init_load_path () = (* additional ml directories, given with option -I *) List.iter Mltop.add_ml_dir (List.rev !ml_includes) -let init_library_roots () = - includes := [] - (* Initialises the Ocaml toplevel before launching it, so that it can find the "include" file in the *source* directory *) let init_ocaml_path () = |