]> matita.cs.unibo.it Git - helm.git/blobdiff - components/library/librarian.mli
irediced usage of matita.includes, that is now set by
[helm.git] / components / library / librarian.mli
index 5280dbbf8a4c0460647380d4ad08117731ca025e..90b7ef168e64a265a1f24400a4846fa5ea2c0568 100644 (file)
@@ -4,11 +4,13 @@ val find_root: string -> string
 
 val parse_root: string -> (string*string) list
 
-(* baseuri_of_script ?(inc:REG[matita.includes]) fname -> root, buri, fullpath 
+(* baseuri_of_script ?(inc:REG[matita.includes]) fname 
+ *   -> 
+ * root, buri, fullpath, rootrelativepath
  * sample: baseuri_of_script a.ma -> /home/pippo/devel/, cic:/matita/a,
  * /home/pippo/devel/a.ma *)
 val baseuri_of_script: 
-  ?include_paths:string list -> string -> string * string * string
+  ?include_paths:string list -> string -> string * string * string * string
 
 (* finds all the roots files in the specified dir *)
 val find_roots_in_dir: string -> string list