From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 5 Apr 2011 15:59:50 +0000 (+0000)
Subject: we removed an extra dot from the "include" syntax
X-Git-Tag: make_still_working~2536
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6d66293a79136e2ff290441b19fb18d2f667fed4;p=helm.git

we removed an extra dot from the "include" syntax
---

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