grafite parser updated

[helm.git] / matita / components / statuses.txt

diff --git a/matita/components/statuses.txt b/matita/components/statuses.txt
index e6276014b23d8f772454f6755fc60c8a46978078..285eae584ff381b10ea3f305ab260cc7d33e7885 100644 (file)
--- a/matita/components/statuses.txt
+++ b/matita/components/statuses.txt
@@ -1,5 +1,5 @@
 grafitetypes(baseuri,ng_mode)
- |--> dumpable(dump)
+ |--> dumpable(dump=objs+dependencies+includes)
  |--> nciclibrary(timestamp)
  |--> grafiteparser(db=ast_statement grammarentry)
  |     |--> cicnotationparser(db=grammars+keywords+items)