equal
deleted
inserted
replaced
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 |