diff options
author | Andrei Pavel <andrei@isc.org> | 2023-05-13 17:02:05 +0200 |
---|---|---|
committer | Andrei Pavel <andrei@isc.org> | 2023-05-13 17:02:05 +0200 |
commit | 14bcae7fac63d169d32e2ee05d90022a37f8dd0a (patch) | |
tree | 5d0f37b1b0b6452fade8e13cbdcd0f0ac0975a01 /tools/check-for-json-errors-in-doc.sh | |
parent | [#2822] fixed check tool and documentation (diff) | |
download | kea-14bcae7fac63d169d32e2ee05d90022a37f8dd0a.tar.xz kea-14bcae7fac63d169d32e2ee05d90022a37f8dd0a.zip |
[#2822] add check-for-json-errors-in-doc.sh to CI
Diffstat (limited to 'tools/check-for-json-errors-in-doc.sh')
-rwxr-xr-x | tools/check-for-json-errors-in-doc.sh | 20 |
1 files changed, 18 insertions, 2 deletions
diff --git a/tools/check-for-json-errors-in-doc.sh b/tools/check-for-json-errors-in-doc.sh index b8c96a4984..a748cfb07d 100755 --- a/tools/check-for-json-errors-in-doc.sh +++ b/tools/check-for-json-errors-in-doc.sh @@ -1,14 +1,26 @@ #!/bin/bash + +# Usage: +# check-for-json-errors-in-doc.sh [--all] [<file1>, <file2>, ...] + # Change directory to the root of the repository. script_path=$(cd "$(dirname "${0}")" && pwd) cd "${script_path}/.." + # Parse parameters. if test ${#} -gt 0; then - files="${*}" + if test "${1}" = '--all'; then + files='doc src' + else + files="${*}" + fi else - files='doc src' + # By default, check only modified files. + files=$(git diff --name-only $(git merge-base origin/master HEAD)) fi +exit_code=0 + # Get the files. files=$(find ${files} -type f \( -name '*.rst' -or -name '*.json' \) -and -not -path '*/_build/*' -and -not -path '*/man/*' | sort) work_file=$(mktemp) @@ -48,6 +60,7 @@ for file in $files; do echo "===start of JSON block===" cat $work_file echo "====end of JSON block====" + exit_code=1 fi fi if [ $comment -eq 0 -a $json -eq 1 ]; then @@ -86,7 +99,10 @@ for file in $files; do echo "===start of JSON block===" cat $work_file echo "====end of JSON block====" + exit_code=1 fi fi done rm $work_file + +exit ${exit_code} |