- let tmp_db_name =
- if HExtlib.is_dir "/dev/shm/" && HExtlib.writable_dir "/dev/shm/" then
- ((*HLog.debug "using /dev/shm to store the working copy of the db";*)
- "/dev/shm/matita.db." ^ username ^ "." ^ string_of_int (Unix.getpid ()))
- else
- ((*HLog.debug "/dev/shm not available";*)
- Helm_registry.get "matita.basedir" ^ "/matita.db." ^ username ^ "." ^
- string_of_int (Unix.getpid ()))
- in
- let db_name = Helm_registry.get "matita.basedir" ^ "/" ^ database ^ ".db" in
- let standard_db_name =
- Helm_registry.get "matita.rt_base_dir" ^ "/metadata.db"
+ let host_mangled = Pcre.replace ~pat:"[/ .]" ~templ:"_" host in
+ let tmp_db_name =
+ "/dev/shm/matita.db." ^ username ^ "." ^ host_mangled ^ "." ^
+ string_of_int (Unix.getpid ())