Re-add has_public_example to circleci.sh for legacy compatibility

dlang · Jun 26, 2017 · 5cc58f9 · 5cc58f9
1 parent 9f82a92
commit 5cc58f9
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/circleci.sh b/circleci.sh
@@ -139,5 +139,7 @@ case $1 in
     coverage) coverage ;;
     publictests) publictests ;;
     style_lint) style_lint ;;
+    # has_public_example has been removed and is kept for compatibility with older PRs
+    has_public_example) echo "OK" ;;
     *) echo "Unknown command"; exit 1;;
 esac