X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Flibrary%2Flibrarian.ml;h=13fccbfa25479beee0e52634cc75ebddf7dbf2ec;hb=b3afed9fd3cc38ecd4578f6b0741be50872a2828;hp=9ffde2b87d0444c6d9ad012b4e26e9641d45a513;hpb=2e17165ef9e63367cc290ad555145b4c22a4582b;p=helm.git

diff --git a/matita/components/library/librarian.ml b/matita/components/library/librarian.ml
index 9ffde2b87..13fccbfa2 100644
--- a/matita/components/library/librarian.ml
+++ b/matita/components/library/librarian.ml
@@ -111,8 +111,12 @@ let find_root_for ~include_paths file =
 
 let mk_baseuri root extra =
   let chop name = 
+(* FG: there is no reason why matita should edit just matita files
+       matita's editor is good on its own and has interesting facilities
+       including predefined virtuals
     assert(Filename.check_suffix name ".ma" ||
       Filename.check_suffix name ".mma");
+*)    
     try Filename.chop_extension name
     with Invalid_argument "Filename.chop_extension" -> name
   in