diff options
Diffstat (limited to 'project')
| -rwxr-xr-x | project | 17 |
1 files changed, 14 insertions, 3 deletions
@@ -41,8 +41,10 @@ make_targets= software_dir= clean_texdir=0 prepare_redo=0 +highlightnew=0 all_highlevel=0 existing_conf=0 +highlightnotes=0 scriptname="./project" minmapsize=10000000000 @@ -118,10 +120,14 @@ Configure and Make options: -j, --jobs=INT Number of threads to build/run the software. -?, --help Print this help list. -Make options: +Make (analysis) options: -d, --debug=FLAGS Print various types of debugging information. -p, --prepare-redo Re-do preparation (only done automatically once). +Make (final PDF) options: + --highlight-new Highlight '\new' parts of text as green. + --highlight-notes Show '\tonote' regions as red text in PDF. + Mandatory or optional arguments to long options are also mandatory or optional for any corresponding short options. @@ -205,6 +211,10 @@ do # # Note that Make's `debug' can take values, but when called without any # value, it is like giving it a value of `a'): + --highlight-new) highlightnew=1; shift;; + --highlight-new=*) on_off_option_error --highlight-new;; + --highlight-notes) highlightnotes=1; shift;; + --highlight-notes=*) on_off_option_error --highlight-notes;; -d|--debug) if [ x"$2" = x ]; then debug=a; shift; else debug="$2"; check_v debug "$debug"; shift;shift; fi;; -d=*|--debug=*) debug="${1#*=}"; check_v debug "$debug"; shift;; @@ -370,8 +380,9 @@ controlled_env() { # Remove all existing environment variables (with `env -i') and only # use some pre-defined environment variables, then build the project. envmake=".local/bin/env -i HOME=$bdir sys_rm=$(which rm) $gopt" - envmake="$envmake .local/bin/make --no-builtin-rules" - envmake="$envmake --no-builtin-variables -f $1" + envmake="$envmake highlightnew=$highlightnew" + envmake="$envmake highlightnotes=$highlightnotes .local/bin/make" + envmake="$envmake --no-builtin-rules --no-builtin-variables -f $1" if ! [ x"$debug" = x ]; then envmake="$envmake --debug=$debug"; fi # Set the number of jobs. Note that for the `configure.sh' script the |