2018-11-26 17:39:20 -08:00
|
|
|
#!/usr/bin/env bash
|
|
|
|
|
set -e
|
|
|
|
|
|
|
|
|
|
cd "$(dirname "$0")"
|
|
|
|
|
|
2019-12-29 18:15:32 -08:00
|
|
|
# md check
|
|
|
|
|
find src -name '*.md' -a \! -name SUMMARY.md |
|
|
|
|
|
while read -r file; do
|
|
|
|
|
if ! grep -q '('"${file#src/}"')' src/SUMMARY.md; then
|
|
|
|
|
echo "Error: $file missing from SUMMARY.md"
|
|
|
|
|
exit 1
|
|
|
|
|
fi
|
|
|
|
|
done
|
|
|
|
|
|
|
|
|
|
|
2019-06-27 15:20:37 -07:00
|
|
|
make -j"$(nproc)" test
|
