--- a/Admin/makerpm Thu May 06 11:48:26 1999 +0200 +++ b/Admin/makerpm Thu May 06 15:34:36 1999 +0200 @@ -172,7 +172,6 @@ $BIN/Isabelle $BIN/isabelle $BIN/isatool -%dir $ISABELLE_HOME EOF for F in $(ls -1 | grep -v heaps | grep -v browser_info)