From eab4837fe057c5b90b2484b7257d115627db6d6f Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 10 Mar 2013 12:01:43 +0000 Subject: [PATCH] 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! --- matita/components/library/librarian.ml | 4 ++++ 1 file changed, 4 insertions(+) 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 -- 2.39.2