diff --git a/tools/check.sh b/tools/check.sh new file mode 100755 index 00000000..3113e768 --- /dev/null +++ b/tools/check.sh @@ -0,0 +1,7 @@ +#!/bin/sh +set -ex +./tools/find-broken-redirects +./tools/find-missing +./tools/find-orphans +./tools/find-whitespace +yamllint docs/