From 84353303cb570874509ee3535b45fe3dfdac6b25 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 11 Jan 2008 15:08:45 +0000 Subject: [PATCH] added a warning if the baseuri we want to clean is read-only --- helm/software/matita/matitacLib.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index c85d2c6bf..0763981c6 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -138,7 +138,11 @@ let compile options fname = then begin HLog.message ("baseuri " ^ baseuri ^ " is not empty"); HLog.message ("cleaning baseuri " ^ baseuri); - LibraryClean.clean_baseuris [baseuri] + LibraryClean.clean_baseuris [baseuri]; + if (not (Http_getter_storage.is_empty ~local:true baseuri)) then begin + HLog.error ("Baseuri "^baseuri^" not cleaned! (probably readonly)"); + exit 1; + end; end; (* create dir for XML files *) if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk" -- 2.39.2