diff -r 1436349f8b28 -r 793b33191ce3 Admin/makerpm
--- a/Admin/makerpm	Sat May 01 00:10:05 1999 +0200
+++ b/Admin/makerpm	Mon May 03 10:47:32 1999 +0200
@@ -183,7 +183,7 @@
 
 # invoke rpm
 
-chgrp -R isabelle "$TMP"
+chown -R root:root "$TMP" || chgrp -R isabelle "$TMP"
 
 echo "topdir: $TMP" >"$TMP/rpmrc"
 rpm --rcfile "$TMP/rpmrc" -bb "$TMP/SPECS/isabelle.spec"