feat: agd NO_BUILD option

Agoric · Oct 6, 2023 · 81201cc · 81201cc
1 parent b5abe88
commit 81201cc
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/bin/agd b/bin/agd
@@ -91,6 +91,7 @@ if $NEED_NODEJS; then
 fi
 
 (
+  ${NO_BUILD:-false} && exit 0
   # Send the build output to stderr unless we're only building.  This prevents
   # the daemon's stdout from being polluted with build output.
   $BUILD_ONLY || exec 1>&2