From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 10 Mar 2013 12:01:43 +0000 (+0000)
Subject: we removed a useless assertion that was forcing matita to edit just matita files
X-Git-Tag: make_still_working~1226
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=eab4837fe057c5b90b2484b7257d115627db6d6f;p=helm.git

we removed a useless assertion that was forcing matita to edit just matita files
matita's editor is good on its own and has interesting facilities including predefined virtuals
in lambdadelta we use matita to edit the .tbl files containing notation from the .ma's
and we use matita as well to edit predefined_virtuals.ml
we still wonder how we could do this up to now despite the assertion!
---

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