diff options
| author | Colin Davidson <colrdavidson@gmail.com> | 2022-03-09 06:14:30 -0800 |
|---|---|---|
| committer | Colin Davidson <colrdavidson@gmail.com> | 2022-03-09 06:14:30 -0800 |
| commit | f5cc8bd7bf0071d46fb39091a23fe19def22c02b (patch) | |
| tree | 46e7d0cf2765f03a80016512b5a915acbb9120c7 | |
| parent | 005d52cab7db883269e325ca8c0bb9e56a6e542e (diff) | |
only build odin for report when necessary
| -rwxr-xr-x | build_odin.sh | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/build_odin.sh b/build_odin.sh index 634e4aa7f..77d69a6e5 100755 --- a/build_odin.sh +++ b/build_odin.sh @@ -89,8 +89,11 @@ fi if [[ $# -eq 1 ]]; then case $1 in report) - EXTRAFLAGS="-g" - build_odin + if [[ ! -f "./odin" ]]; then + EXTRAFLAGS="-g" + build_odin + fi + ./odin report exit 0 ;; |