"input" was meant to be "include"

diff --git a/helm/matita/matita.lang b/helm/matita/matita.lang
index 3a10765d9f96f0c324c80e86d12aeaf5daf2ac7e..b28793780d890719bf23c3edbd3c596f3cdd05ea 100644 (file)
--- a/helm/matita/matita.lang
+++ b/helm/matita/matita.lang
@@ -23,7 +23,7 @@
   </keyword-list>
     
   <keyword-list _name = "Commands" style = "Keyword" case-sensitive="TRUE">
-    <keyword>input</keyword>
+    <keyword>include</keyword>
     <keyword>alias</keyword>
     <keyword>coercion</keyword>
     <keyword>coinductive</keyword>