summaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rwxr-xr-xbuild.sh3
1 files changed, 3 insertions, 0 deletions
diff --git a/build.sh b/build.sh
index 18bd60c5..3cf89a14 100755
--- a/build.sh
+++ b/build.sh
@@ -64,6 +64,9 @@ for BUILD_TARGET_LC in $(subst_tgts invariants ${BUILD_TARGETS_META:-world}); do
else
(set -o errexit -o noglob;
parse_with_pkg_name "${BUILD_PACKAGE_LC%.*}";
+ if is_build_script_done finish; then
+ exit 0;
+ fi;
for __ in ${BUILD_STEPS}; do
case ${__#*:} in
abstract)