Admin/isatest-makeall
changeset 13233 5ab7bac534c9
parent 13232 8b1b5e8c4bd6
child 13236 568bc754d303
     1.1 --- a/Admin/isatest-makeall	Thu Jun 20 22:17:15 2002 +0200
     1.2 +++ b/Admin/isatest-makeall	Thu Jun 20 22:17:28 2002 +0200
     1.3 @@ -58,12 +58,14 @@
     1.4  
     1.5      echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
     1.6  
     1.7 -    cp -v $SETTINGS $DISTPREFIX/Isabelle/etc/settings >> $TESTLOG 2>&1 
     1.8 +    cp $DISTPREFIX/Isabelle/etc/settings $DISTPREFIX/Isabelle/etc/settings.save-$SHORT
     1.9 +    cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
    1.10      $DISTPREFIX/Isabelle/bin/isatool makeall all >> $TESTLOG 2>&1 
    1.11  
    1.12      if [ $? -eq 0 ]
    1.13      then
    1.14          echo ------------------- test successfull --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
    1.15 +        mv $DISTPREFIX/Isabelle/etc/settings-$SHORT $DISTPREFIX/Isabelle/etc/settings
    1.16          gzip -f $TESTLOG
    1.17      else
    1.18          echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1