From 6d66293a79136e2ff290441b19fb18d2f667fed4 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 5 Apr 2011 15:59:50 +0000 Subject: [PATCH] we removed an extra dot from the "include" syntax --- matita/components/grafite/grafiteAstPp.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml index 48fc8691c..eda934d68 100644 --- a/matita/components/grafite/grafiteAstPp.ml +++ b/matita/components/grafite/grafiteAstPp.ml @@ -178,9 +178,9 @@ let pp_ncommand status = function map) | Include (_,mode,path) -> (* not precise, since path is absolute *) if mode = WithPreferences then - "include \"" ^ path ^ "\"." + "include \"" ^ path ^ "\"" else - "include' \"" ^ path ^ "\"." + "include' \"" ^ path ^ "\"" | Alias (_,s) -> pp_alias s | Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) -> pp_interpretation dsc symbol arg_patterns cic_appl_pattern -- 2.39.2