# HG changeset patch
# User wenzelm
# Date 878725155 -3600
# Node ID af6743b065fbe70183572ab462e9a3f672c2e47d
# Parent  2ce2e659c2b1e770b56a4a796ffa9d2fffd9a55a
base root = "";

diff -r 2ce2e659c2b1 -r af6743b065fb src/Pure/Thy/path.ML
--- a/src/Pure/Thy/path.ML	Wed Nov 05 09:08:35 1997 +0100
+++ b/src/Pure/Thy/path.ML	Wed Nov 05 11:19:15 1997 +0100
@@ -36,6 +36,7 @@
   | absolute _ = false;
 
 fun base (Path []) = ""
+  | base (Path ["/"]) = ""
   | base (Path xs) = snd (split_last xs);