From 0fffe8d30f909612d73b5e927608d881f21423b2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 29 Nov 2000 17:50:09 +0000
Subject: Bug option -I et -R quand le répertoire est '..'

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

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c128332b24..cff15a0034 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -85,7 +85,11 @@ let parse_include d =
   with Not_found ->
     let alias = Filename.basename d in
     let alias =
-      if alias = "." then Filename.basename (Unix.getcwd ()) else alias in
+      if alias = "." then
+	Filename.basename (Unix.getcwd ())
+      else if alias = ".." then
+	Filename.basename (Filename.dirname (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