From 46013cfe393bd89cb92e3703955c259685bac551 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 5 Sep 2005 10:04:00 +0000
Subject: [PATCH] The popup that asks to generate .moo for a .ma shows only the
 basename and not the full path of the file.

---
 helm/matita/matitaGui.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 = 
-- 
2.39.2