From 684613eccdbb3ed57e593d6f501854ca3af4aa1d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 29 Nov 2000 17:14:53 +0000
Subject: Bug option -I et -R quand le répertoire est '.'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1035 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/coqtop.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 53163a4a15..c128332b24 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -84,6 +84,8 @@ let parse_include d =
      Names.dirpath_of_string (String.sub d (pos+1) (String.length d - pos -1)))
   with Not_found ->
     let alias = Filename.basename d in
+    let alias =
+      if alias = "." then Filename.basename (Unix.getcwd ()) else alias in
     if not (Names.is_ident alias) then 
       error ("Cannot find a name to which "^d^" may map in Coq library");
     (d, [alias])
-- 
cgit v1.2.3