diff --git a/Doc/tools/mkhowto.sh b/Doc/tools/mkhowto.sh index 6fa83b2006a..1038954f6a5 100755 --- a/Doc/tools/mkhowto.sh +++ b/Doc/tools/mkhowto.sh @@ -376,4 +376,6 @@ for FILE in $@ ; do rm -f $LOGFILE done -rm -f $L2H_AUX_INIT_FILE +if [ ! "$DEBUGGING" ] ; then + rm -f $L2H_AUX_INIT_FILE +fi