Admin/build
changeset 64370 865b39487b5d
parent 58791 00916b0dd596
child 71367 91d5a8255c98
equal deleted inserted replaced
64369:6a9816764b37 64370:865b39487b5d
    24   The MODULES list may contain any of the following:
    24   The MODULES list may contain any of the following:
    25 
    25 
    26     all             all modules below
    26     all             all modules below
    27     browser         graph browser
    27     browser         graph browser
    28     jars            Isabelle/Scala
    28     jars            Isabelle/Scala
    29     jars_test       test separate build of jars
       
    30     jars_fresh      fresh build of jars
    29     jars_fresh      fresh build of jars
    31 
    30 
    32 EOF
    31 EOF
    33   exit 1
    32   exit 1
    34 }
    33 }
    84   case $MODULE in
    83   case $MODULE in
    85     all) build_all;;
    84     all) build_all;;
    86     browser) build_browser;;
    85     browser) build_browser;;
    87     jars) build_jars;;
    86     jars) build_jars;;
    88     jars_fresh) build_jars -f;;
    87     jars_fresh) build_jars -f;;
    89     jars_test) build_jars -t;;
       
    90     *) fail "Bad module $MODULE"
    88     *) fail "Bad module $MODULE"
    91   esac
    89   esac
    92 done
    90 done