diff options
| -rwxr-xr-x | project/scripts/genDocs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/project/scripts/genDocs b/project/scripts/genDocs index d18a583be..73e034276 100755 --- a/project/scripts/genDocs +++ b/project/scripts/genDocs @@ -6,7 +6,7 @@ set -e # set extended glob, needed for rm everything but x shopt -s extglob -if [ "$1" = "test" ]; then +if [ "$1" = ";dotty-compiler/testOnly dotty.tools.dotc.CompilationTests" ]; then # make sure that BOT_PASS is set if [ -z ${2+x} ]; then |