diff options
| author | Jérémy Zurcher <jeremy@asynk.ch> | 2022-07-17 23:27:21 +0200 |
|---|---|---|
| committer | Jérémy Zurcher <jeremy@asynk.ch> | 2022-07-17 23:27:21 +0200 |
| commit | ddb77225b046a0da2870c80aa3d4ca35755a5a71 (patch) | |
| tree | b3d878af08ff863e8734aa5be5608d4cd3f46cdb /godot-update | |
| parent | 0a1e1f794cc1ddfafc90debbb0dc825f5ca71dd6 (diff) | |
| download | bin-ddb77225b046a0da2870c80aa3d4ca35755a5a71.zip bin-ddb77225b046a0da2870c80aa3d4ca35755a5a71.tar.gz | |
godot-update : small fix
Diffstat (limited to 'godot-update')
| -rwxr-xr-x | godot-update | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/godot-update b/godot-update index 06b9003..5f03399 100755 --- a/godot-update +++ b/godot-update @@ -39,6 +39,7 @@ function build() export CXX=/usr/lib/ccache/bin/clang++ export CC=/usr/lib/ccache/bin/clang + [ -f custom.py ] && rm custom.py rm ./bin/* platform=linuxbsd platform=x11 @@ -94,17 +95,16 @@ pushd $DIR HEAD_NOW=$(git log HEAD~1.. --pretty=format:'%H' | head -n1) echo -e "updated HEAD : $RED$HEAD_NOW$RESET" - if [ $FORCE = 1 -o "$HEAD_PREV" != "$HEAD_NOW" ] + if [ $FORCE = 1 ] || [ "$HEAD_PREV" != "$HEAD_NOW" ] then build git log $HEAD_PREV.. fi + strip ./bin/godot.* + ls -lh ./bin/ popd -strip $DIR/bin/godo.* -ls -lh $DIR/bin/ - # https://godot-build-options-generator.github.io # scons -j4 platform=linuxbsd target=release_debug tools=yes pulseaudio=no bits=64 warnings=no #custom_modules=../modules # scons -j4 platform=android target=debug android_arch=arm64v8 ndk_platform=android-22 tools=no disable_3d=true |