The popup that asks to generate .moo for a .ma shows only the basename and not the...

[helm.git] / helm / matita / matitaGui.ml

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index fbae8013de79850c353f46628d49bc1f584b6464..3c323a3c2e090596601deafa9a1188ed0be4ef26 100644 (file)
--- 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 =