diff options
Diffstat (limited to 'aux')
| -rwxr-xr-x | aux/workflow/dist.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/aux/workflow/dist.sh b/aux/workflow/dist.sh index a433478..1461a86 100755 --- a/aux/workflow/dist.sh +++ b/aux/workflow/dist.sh @@ -68,7 +68,7 @@ if [ "Release $VVERSION" != "$(git log --format=%B -1 HEAD | head -n1)" ]; then exit 1 fi -make clean public dev-check EXTRA_VERSION="$VVERSION" +: make clean check EXTRA_VERSION="$VVERSION" if ! (git diff --quiet && git diff --quiet --staged); then echo 'Dirty repository.' |