From 92f79e6e3007617791dfb65034e39dd29aa0296f Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Tue, 21 Jun 2011 15:06:43 +0000 Subject: [PATCH] Changed user library dir to users/ --- matitaB/matita/matitaFilesystem.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/matitaB/matita/matitaFilesystem.ml b/matitaB/matita/matitaFilesystem.ml index fe67b256b..df4d4f844 100644 --- a/matitaB/matita/matitaFilesystem.ml +++ b/matitaB/matita/matitaFilesystem.ml @@ -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 -- 2.39.2