update scripts/gen.sh

ilius · Dec 28, 2024 · 81d6bf1 · 81d6bf1
1 parent abd522f
commit 81d6bf1
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/scripts/gen.sh b/scripts/gen.sh
@@ -3,6 +3,9 @@ set -e
 
 myDir1=$(dirname "$0")
 
+# to handle rename of a plugin:
+rm $myDir1/../doc/p/*.md
+
 set -x
 
 python "$myDir1/plugin-index.py"