From 469c6be3677c365295fd233319db792385e5c688 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sat, 10 Sep 2016 13:05:50 +0200
Subject: Avoid putting a useless "toploop" directory in the ML search path if
 it does not exist.

---
 toplevel/coqinit.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 258a1135fc..8a8dbe9601 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -89,7 +89,8 @@ let init_load_path () =
       Mltop.add_ml_dir (coqlib/"stm");
       Mltop.add_ml_dir (coqlib/"ide")
     end;
-    Mltop.add_ml_dir (coqlib/"toploop");
+    if System.exists_dir (coqlib/"toploop") then
+      Mltop.add_ml_dir (coqlib/"toploop");
     (* then standard library *)
     add_stdlib_path ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false;
     (* then plugins *)
-- 
cgit v1.2.3