diff options
| author | Oliver Smith <osmith@sysmocom.de> | 2022-06-30 11:46:37 +0200 |
|---|---|---|
| committer | Oliver Smith <osmith@sysmocom.de> | 2022-06-30 15:30:00 +0200 |
| commit | 26a02acdf07bb1751aa2cffbb9ffa1fe785f5638 (patch) | |
| tree | 1f2e15592c6150247b60f1ecb2f75fa51a28db03 | |
| parent | 12630c87ab515602a127562bb846ccc92e9facb8 (diff) | |
coverity/prepare_source: add SRC_SKIP_FETCH/CLEAN
When running these scripts locally while developing, it's more useful to
not fetch the sources and clean the git repository instead. Add
environment variables that allow doing this.
Change-Id: Id6d3cdabb776435df36c0145d93e514693062fca
| -rwxr-xr-x | coverity/prepare_source_Osmocom.sh | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/coverity/prepare_source_Osmocom.sh b/coverity/prepare_source_Osmocom.sh index 09608eb..452af3e 100755 --- a/coverity/prepare_source_Osmocom.sh +++ b/coverity/prepare_source_Osmocom.sh @@ -38,7 +38,12 @@ for proj in \ ; do if [ -d $proj ]; then - (cd $proj && git fetch && git checkout -f -B master origin/master) + if [ -z "$SRC_SKIP_FETCH" ]; then + (cd $proj && git fetch && git checkout -f -B master origin/master) + fi + if [ -n "$SRC_CLEAN" ]; then + git -C "$proj" clean -ffxd + fi else git clone git://git.osmocom.org/$proj fi |