Admin/isatest/isatest-stats
changeset 25547 ffa6e91b7add
parent 24831 887d1b32a1a5
child 26172 fa302c5bc2f2
equal deleted inserted replaced
25546:4f8d7ac83c0b 25547:ffa6e91b7add
     5 #
     5 #
     6 # DESCRIPTION: Standard statistics.
     6 # DESCRIPTION: Standard statistics.
     7 
     7 
     8 THIS=$(cd "$(dirname "$0")"; pwd -P)
     8 THIS=$(cd "$(dirname "$0")"; pwd -P)
     9 
     9 
    10 PLATFORMS="at-poly at-sml-dev at64-poly-e at64-poly-5.1-para-e at-mac-poly-5.1-para-e afp"
    10 PLATFORMS="at-poly at-sml-dev at64-poly at64-poly-5.1-para at-mac-poly-5.1-para afp"
    11 
    11 
    12 ISABELLE_SESSIONS="\
    12 ISABELLE_SESSIONS="\
    13   HOL \
    13   HOL \
    14   HOL-Algebra \
    14   HOL-Algebra \
    15   HOL-Auth \
    15   HOL-Auth \