From 5143973417de0bd6796554c0fd45dbf9424ee07e Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 9 Jan 2006 12:51:58 +0000 Subject: [PATCH] added cleaning of .lexicon and .metadata files --- helm/matita/matitaclean.ml | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/helm/matita/matitaclean.ml b/helm/matita/matitaclean.ml index 2a47bd1e4..826a4a282 100644 --- a/helm/matita/matitaclean.ml +++ b/helm/matita/matitaclean.ml @@ -30,6 +30,8 @@ open Printf module UM = UriManager module TA = GrafiteAst +let clean_suffixes = [ ".moo"; ".lexicon"; ".metadata"; ".xml.gz" ] + let main () = let _ = MatitaInit.initialize_all () in let basedir = Helm_registry.get "matita.basedir" in @@ -37,11 +39,13 @@ let main () = | [ "all" ] -> LibraryDb.clean_owner_environment (); let xmldir = basedir ^ "/xml" in - ignore - (Sys.command - ("find " ^ xmldir ^ - " \\( -name \\*.xml.gz -o -name \\*.moo \\) " ^ - "-exec rm \\{\\} \\; 2> /dev/null")); + let clean_pat = + String.concat " -o " + (List.map (fun suf -> "-name \\*" ^ suf) clean_suffixes) in + let clean_cmd = + sprintf "find %s \\( %s \\) -exec rm \\{\\} \\; 2> /dev/null" + xmldir clean_pat in + ignore (Sys.command clean_cmd); ignore (Sys.command ("find " ^ xmldir ^ " -type d -exec rmdir -p {} \\; 2> /dev/null")); -- 2.39.2