fix cleaning in library scripts (#1054)

Deducteam · Feb 22, 2024 · 4e2d68f · 4e2d68f
1 parent 9597727
commit 4e2d68f
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/libraries/holide.sh b/libraries/holide.sh
@@ -5,8 +5,9 @@ DIR="holide"
 
 # Cleaning command (clean and exit).
 if [[ "$#" -eq 1 && ("$1" = "clean" || "$1" = "fullclean") ]]; then
-  rm -rf ${DIR}
+  if [[ -d ${DIR} ]]; then find ${DIR} -name '*.lpo' -delete; fi
   if [[ "$1" = "fullclean" ]]; then
+    if [[ -d ${DIR} ]]; then find ${DIR} -name '*.dk' -delete; fi
     rm -f holide.tar.gz
   fi
   exit 0

diff --git a/libraries/matita.sh b/libraries/matita.sh
@@ -5,8 +5,9 @@ DIR="matita"
 
 # Cleaning command (clean and exit).
 if [[ "$#" -eq 1 && ("$1" = "clean" || "$1" = "fullclean") ]]; then
-  rm -rf ${DIR}
+  if [[ -d ${DIR} ]]; then find ${DIR} -name '*.lpo' -delete; fi
   if [[ "$1" = "fullclean" ]]; then
+    if [[ -d ${DIR} ]]; then find ${DIR} -name '*.dk' -delete; fi
     rm -f matita.tar.gz
   fi
   exit 0