Admin/make_everything
changeset 17572 81fcc0029761
parent 16328 49c1f9dedc56
     1.1 --- a/Admin/make_everything	Wed Sep 21 19:16:16 2005 +0200
     1.2 +++ b/Admin/make_everything	Wed Sep 21 20:16:34 2005 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4  REPOS=~/isabelle/src
     1.5  DIST=~/tmp/isadist
     1.6  
     1.7 -$REPOS/Admin/makedist ${1:---}
     1.8 +$REPOS/Admin/makedist ${1:--}
     1.9  ISABELLE_DIST=$(cat $DIST/ISABELLE_DIST)
    1.10  
    1.11  case $(hostname) in