Skip to content

Commit 8cba990

Browse files
Don’t try to validate trace XML when xmllint not found
This was the intended behaviour to begin with, I just forgot to put the ‘exit’ there.
1 parent 7d30335 commit 8cba990

File tree

1 file changed

+1
-0
lines changed
  • regression/validate-trace-xml-schema

1 file changed

+1
-0
lines changed

regression/validate-trace-xml-schema/check.sh

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ fi
1313
xmllint="$(command -v xmllint)"
1414
if [ $? -ne 0 ] > /dev/null; then
1515
echo "xmllint not found, skipping XSD tests"
16+
exit
1617
fi
1718

1819
python3 check.py ../../src/cbmc/cbmc "$xmllint"

0 commit comments

Comments
 (0)