aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar Paul Steckler <steck@stecksoft.com>2017-12-05 11:04:42 -0500
committerGravatar Paul Steckler <steck@stecksoft.com>2017-12-05 11:04:42 -0500
commit511d3ed44705c58234b95b65500f9f597d56c7cf (patch)
tree0d3ddbf5661db9aa3ac5a46d4b54266de8f59a21 /ide
parent0048cbe810c82a775558c14cd7fcae644e205c51 (diff)
Don't Add LoadPath on CoqIDE startup, #6153
Diffstat (limited to 'ide')
-rw-r--r--ide/ide_slave.ml9
1 files changed, 1 insertions, 8 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index cfc0e09a0..43d7aa363 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -377,15 +377,8 @@ let init =
match file with
| None -> init_sid
| Some file ->
- let dir = Filename.dirname file in
- let open Loadpath in let open CUnix in
let doc, initial_id, _ =
- let doc = get_doc () in
- if not (is_in_load_paths (physical_path_of_string dir)) then begin
- let pa = Pcoq.Gram.parsable (Stream.of_string (Printf.sprintf "Add LoadPath \"%s\". " dir)) in
- let loc_ast = Stm.parse_sentence ~doc init_sid pa in
- Stm.add false ~doc ~ontop:init_sid loc_ast
- end else doc, init_sid, `NewTip in
+ get_doc (), init_sid, `NewTip in
if Filename.check_suffix file ".v" then
Stm.set_compilation_hints file;
set_doc (Stm.finish ~doc);