diff --git a/scripts/gen.sh b/scripts/gen.sh index 23e703730..908b5b17c 100755 --- 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"