Update test_merge_branch to check if all the documentation headers actually exist.

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
+    
+  
+

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