diff options
Diffstat (limited to 'scripts')
| -rw-r--r-- | scripts/Makefile | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/scripts/Makefile b/scripts/Makefile index 71976971..1003c0b7 100644 --- a/scripts/Makefile +++ b/scripts/Makefile @@ -20,3 +20,7 @@ test: all dont-run-trang: touch *.rng + +relaxng: left-right-protocol-samples/.stamp + xmllint --noout --relaxng left-right-schema.rng left-right-protocol-samples/*.xml + xmllint --noout --relaxng up-down-schema.rng up-down-protocol-samples/*.xml |