we removed a useless assertion that was forcing matita to edit just matita files

[helm.git] / matita / components / library / librarian.ml

diff --git a/matita/components/library/librarian.ml b/matita/components/library/librarian.ml
index 9ffde2b87d0444c6d9ad012b4e26e9641d45a513..13fccbfa25479beee0e52634cc75ebddf7dbf2ec 100644 (file)
--- 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