diff --git a/doc/htmlize b/doc/htmlize index d8eb69196c..8784dda0ab 100755 --- a/doc/htmlize +++ b/doc/htmlize @@ -25,8 +25,6 @@ foreach document ($1) echo " Cleaning and making $document.ps" -goto doit - make clean >& /dev/null make $document.ps >& $document.latex.log