From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 5 Sep 2005 10:04:00 +0000 (+0000)
Subject: The popup that asks to generate .moo for a .ma shows only the basename and not the... 
X-Git-Tag: V_0_1_2_1~112
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=46013cfe393bd89cb92e3703955c259685bac551;p=helm.git

The popup that asks to generate .moo for a .ma shows only the basename and not the full path of the file.
---

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index fbae8013d..3c323a3c2 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -80,7 +80,7 @@ let ask_and_save_moo_if_needed parent fname status =
         ~title:"A .moo can be generated"
         ~message:(Printf.sprintf 
           "%s can be generated for %s.\n<i>Should I generate it?</i>"
-          mooname fname)
+          (Filename.basename mooname) (Filename.basename fname))
         ~parent ()
       in
       let b =