]> matita.cs.unibo.it Git - helm.git/commitdiff
Changed user library dir to users/
authorWilmer Ricciotti <ricciott@cs.unibo.it>
Tue, 21 Jun 2011 15:06:43 +0000 (15:06 +0000)
committerWilmer Ricciotti <ricciott@cs.unibo.it>
Tue, 21 Jun 2011 15:06:43 +0000 (15:06 +0000)
matitaB/matita/matitaFilesystem.ml

index fe67b256b714dcebfdc66eae1ab404125b7f3979..df4d4f844758822ee5ec5acdc0100c05170da813 100644 (file)
@@ -93,7 +93,7 @@ let html_of_library uid =
     branch (Filename.basename path) (subdirtags ^ "\n" ^ scripttags)
   in
 
-  let basedir = (Helm_registry.get "matita.rt_base_dir") ^ "/lib/" ^ uid ^ "/" in
+  let basedir = (Helm_registry.get "matita.rt_base_dir") ^ "/users/" ^ uid ^ "/" in
   let res = aux basedir in
   prerr_endline "BEGIN TREE";prerr_endline res;prerr_endline "END TREE";
   res