diff -r df9b0abf77e0 -r 927def00b1c6 Admin/makerpm
--- 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)