base root = "";
authorwenzelm
Wed Nov 05 11:19:15 1997 +0100 (1997-11-05)
changeset 4138af6743b065fb
parent 4137 2ce2e659c2b1
child 4139 e1659fd7a221
base root = "";
src/Pure/Thy/path.ML
     1.1 --- a/src/Pure/Thy/path.ML	Wed Nov 05 09:08:35 1997 +0100
     1.2 +++ b/src/Pure/Thy/path.ML	Wed Nov 05 11:19:15 1997 +0100
     1.3 @@ -36,6 +36,7 @@
     1.4    | absolute _ = false;
     1.5  
     1.6  fun base (Path []) = ""
     1.7 +  | base (Path ["/"]) = ""
     1.8    | base (Path xs) = snd (split_last xs);
     1.9  
    1.10