lib/Tools/build
changeset 48578 21361b6189a6
parent 48570 0c32d6267b93
child 48592 a125b8040ada
equal deleted inserted replaced
48577:1edc81c78079 48578:21361b6189a6
    28   echo "  Options are:"
    28   echo "  Options are:"
    29   echo "    -a           select all sessions"
    29   echo "    -a           select all sessions"
    30   echo "    -b           build heap images"
    30   echo "    -b           build heap images"
    31   echo "    -d DIR       include session directory with ROOT file"
    31   echo "    -d DIR       include session directory with ROOT file"
    32   echo "    -g NAME      select session group NAME"
    32   echo "    -g NAME      select session group NAME"
    33   echo "    -j INT       maximum number of jobs (default 1)"
    33   echo "    -j INT       maximum number of parallel jobs (default 1)"
    34   echo "    -n           no build -- test dependencies only"
    34   echo "    -n           no build -- test dependencies only"
    35   echo "    -o OPTION    override session configuration OPTION (via NAME=VAL or NAME)"
    35   echo "    -o OPTION    override session configuration OPTION (via NAME=VAL or NAME)"
    36   echo "    -s           system build mode: produce output in ISABELLE_HOME"
    36   echo "    -s           system build mode: produce output in ISABELLE_HOME"
    37   echo "    -v           verbose"
    37   echo "    -v           verbose"
    38   echo
    38   echo