irediced usage of matita.includes, that is now set by

[helm.git] / components / grafite_parser / grafiteParser.ml

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 07ca6a6f1311218b01401d1f0cb9d8645ef86bd3..c948272ef40ff913d6817275fbfdc4d4b10df460 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -692,7 +692,7 @@ EXTEND
        fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
     | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
        fun ~include_paths status ->
-       let _root, buri, fullpath = 
+       let _root, buri, fullpath, _rrelpath = 
           Librarian.baseuri_of_script ~include_paths fname 
         in
         let status =