diff --git a/Scripts/developer_scripts/check_headers.sh b/Scripts/developer_scripts/check_headers.sh new file mode 100644 index 00000000000..e8cc37d0692 --- /dev/null +++ b/Scripts/developer_scripts/check_headers.sh @@ -0,0 +1,37 @@ +#!bin/bash +PATH_TO_CGAL="$1" +cd $PATH_TO_CGAL +#If set, the pattern ‘**’ used in a filename expansion context +#will match all files and zero or more directories and subdirectories. +#If the pattern is followed by a ‘/’, only directories and subdirectories match. +shopt -s globstar +for DIR in *; do + DOC_DIR=$DIR/doc/$DIR/CGAL + if [ -d "$DOC_DIR" ]; then + cd $DOC_DIR + for DOC_FILE in **/*.h; do + #if the file does not exist in the package + if [ ! -f $PATH_TO_CGAL/$DIR/include/CGAL/$DOC_FILE ]; then + filename=$(basename $DOC_FILE) + cd $PATH_TO_CGAL/ + #search in all of CGAL + OK='false' + #use this syntax to avoid subshell creation + #so that the setting of OK is still good after the loop + while read line; do + if [[ $line != *"doc"* ]]; then + OK='true' + fi + done < <(find -name "$filename") + if [ $OK == 'false' ]; then + echo "$DOC_DIR/$DOC_FILE " + fi + cd $PATH_TO_CGAL/$DOC_DIR + fi + done + cd $PATH_TO_CGAL + fi +done + + + diff --git a/Scripts/developer_scripts/test_merge_of_branch b/Scripts/developer_scripts/test_merge_of_branch index 1412c1f6700..b5a133c7015 100755 --- a/Scripts/developer_scripts/test_merge_of_branch +++ b/Scripts/developer_scripts/test_merge_of_branch @@ -146,6 +146,15 @@ if [ -n "${txt_not_utf8}" ]; then exit 1 fi +#check all headers in documentation actually exist +echo '.. Checking if all documentation headers exist' +not_existing_headers=$(bash ./Scripts/developer_scripts/check_headers.sh $PWD) +if [ -n "${not_existing_headers}" ]; then + echo "The following files are referenced in the documentation but do not exist:" + echo ${not_existing_headers} + exit 1 +fi + current_rev=$(${git} rev-parse HEAD) trap 'echo "(aborting the merge now)" && ${git} reset --quiet --hard ${current_rev}' EXIT