2022-11-03 13:54:49 +00:00
|
|
|
#!/bin/sh
|
|
|
|
|
set -eu
|
2022-11-29 21:54:11 +00:00
|
|
|
if [ ! -d "$(dirname "$0")/ci/sub/.git" ]; then
|
|
|
|
|
git submodule update --init
|
|
|
|
|
fi
|
2022-11-03 13:54:49 +00:00
|
|
|
. "$(dirname "$0")/ci/sub/lib.sh"
|
|
|
|
|
PATH="$(cd -- "$(dirname "$0")" && pwd)/ci/sub/bin:$PATH"
|
|
|
|
|
cd "$(dirname "$0")"
|
|
|
|
|
|
|
|
|
|
_make "$@"
|
