Admin/isatest/isatest-makeall
changeset 28597 e76e7b96a517
parent 28539 bdb308737bfd
child 28982 75f221d67515
equal deleted inserted replaced
28596:fcd463a6b6de 28597:e76e7b96a517
   106   TOOL="$ISABELLE_TOOL makeall $MFLAGS all"
   106   TOOL="$ISABELLE_TOOL makeall $MFLAGS all"
   107 fi
   107 fi
   108 
   108 
   109 # main test loop
   109 # main test loop
   110 
   110 
       
   111 log "starting [$@]"
       
   112 
   111 for SETTINGS in $@; do
   113 for SETTINGS in $@; do
   112 
   114 
   113     [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
   115     [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
   114 
   116 
   115     # logfile setup
   117     # logfile setup