]> matita.cs.unibo.it Git - helm.git/commitdiff
no longer use absolute path for naming notebook labels
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 13 Sep 2005 15:00:48 +0000 (15:00 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 13 Sep 2005 15:00:48 +0000 (15:00 +0000)
helm/matita/matitaScript.ml

index 97c707e51ebedeff5c158432cb4cbe04b7019607..f181b53d291c0d9a64e8755e867b47d70cdc255d 100644 (file)
@@ -449,7 +449,7 @@ object (self)
     
   method private ppFilename =
     match guistuff.filenamedata with 
-    | Some f,_ -> f 
+    | Some f,_ -> Filename.basename 
     | None,_ -> sprintf ".unnamed%d.ma" scriptId
   
   initializer