diff options
author | Rasmus Andersson <rasmus@notion.se> | 2017-09-30 21:45:18 +0300 |
---|---|---|
committer | Rasmus Andersson <rasmus@notion.se> | 2017-09-30 21:45:18 +0300 |
commit | 517a1ff79c146c354db6875ab34c9393f319cbf0 (patch) | |
tree | 09748abb5e3c5789ddbc46c8b470bffc07b8b629 /init.sh | |
parent | c6f7a09c5a8ae3d34e5d984f3bc643f759b5c940 (diff) | |
download | inter-517a1ff79c146c354db6875ab34c9393f319cbf0.tar.xz |
init.sh: adds -f option
Diffstat (limited to 'init.sh')
-rwxr-xr-x | init.sh | 11 |
1 files changed, 10 insertions, 1 deletions
@@ -28,6 +28,13 @@ else set -e cd "$SRCDIR" + if [[ "$1" == "-h" ]] || [[ "$1" == "-help" ]] || [[ "$1" == "--help" ]]; then + echo "usage: $0 [options]" >&2 + echo "options:" >&2 + echo " -f Force generation of build/etc/generated.make" >&2 + exit 1 + fi + # ———————————————————————————————————————————————————————————————————————————————————————————————— # virtualenv @@ -202,7 +209,9 @@ else # Only generate if there are changes to the font sources NEED_GENERATE=false - if [[ ! -f "$GEN_MAKE_FILE" ]] || [[ "$0" -nt "$GEN_MAKE_FILE" ]]; then + if [[ "$1" == "-f" ]]; then + NEED_GENERATE=true + elif [[ ! -f "$GEN_MAKE_FILE" ]] || [[ "$0" -nt "$GEN_MAKE_FILE" ]]; then NEED_GENERATE=true else for style in "${master_styles[@]}"; do |