X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitacLib.ml;h=f248545fba8c6d5caae409eb43fee604273185b2;hb=7a3c40d0d56ba3c20126f1d2c9f651adc95eaef7;hp=70ed5766d273f35db6dbf293aa5313519993faac;hpb=01001c883a8151edba81cd03a6f254d24a81c867;p=helm.git

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index 70ed5766d..f248545fb 100644
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -357,15 +357,18 @@ module F =
         let root,baseuri,_,_ =
           Librarian.baseuri_of_script ~include_paths mafile 
         in
-        let obj =
+        let obj_writeable, obj_read_only =
            if Filename.check_suffix mafile ".mma" then 
+              Filename.chop_suffix mafile ".mma" ^ ".ma",
               Filename.chop_suffix mafile ".mma" ^ ".ma"
            else
               LibraryMisc.obj_file_of_baseuri 
-                        ~must_exist:false ~baseuri ~writable:true
+                        ~must_exist:false ~baseuri ~writable:true,
+              LibraryMisc.obj_file_of_baseuri 
+                        ~must_exist:false ~baseuri ~writable:false
         in
-        Some root, obj 
-      with Librarian.NoRootFor x -> None, ""
+        Some root, obj_writeable, obj_read_only
+      with Librarian.NoRootFor x -> None, "", ""
     ;;
 
     let mtime_of_source_object s =