Run the compiler a second time without -H in case of errors

Installation/CMakeLists.txt

@@ -1278,6 +1278,15 @@ LEDA_FOUND is false.")
               UNIX_COMMAND
               "${CMAKE_CXX_COMPILER} ${compile_options_str}
 ${include_options_str} -x c++ ${flag} -H \
+${CMAKE_CURRENT_SOURCE_DIR}/../${package}/include/${header}"
+              # The header Algebraic_kernel_rs_gmpz_d_1.h is skipped on purpose: it
+              # depends on RS.
+              )
+            # CMD2 is CMD without the -H option
+            separate_arguments(CMD2
+              UNIX_COMMAND
+              "${CMAKE_CXX_COMPILER} ${compile_options_str}
+${include_options_str} -x c++ ${flag} \
 ${CMAKE_CURRENT_SOURCE_DIR}/../${package}/include/${header}"
               # The header Algebraic_kernel_rs_gmpz_d_1.h is skipped on purpose: it
               # depends on RS.
@@ -1288,6 +1297,7 @@ ${CMAKE_CURRENT_SOURCE_DIR}/../${package}/include/${header}"
               COMMAND ${CMAKE_COMMAND}
               -DCERR:STRING=${chk_header_name}
               "-DCMD:STRING=${CMD}"
+              "-DCMD2:STRING=${CMD2}"
               -P "${CGAL_MODULES_DIR}/run_cmd_redirection_cerr.cmake"
               DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/../${package}/include/${header}
               DEPENDS ${CGAL_MODULES_DIR}/run_cmd_redirection_cerr.cmake

Installation/cmake/modules/run_cmd_redirection_cerr.cmake

@@ -17,15 +17,19 @@ endif()
 
 execute_process(
   COMMAND ${CMD}
-  ERROR_VARIABLE err
+  ERROR_FILE "${CERR}"
   OUTPUT_VARIABLE output
   RESULT_VARIABLE error_result)
-
-file(WRITE ${CERR} "${err}")
-
 if(error_result)
-  string(REPLACE ";" " " CMD_STR "${CMD}")
+  if(CMD2)
-  message(SEND_ERROR 
+    file(REMOVE ${CERR})
+    execute_process(COMMAND ${CMD2})
+    message(SEND_ERROR)
+  else()
+    file(READ ${CERR} err)
+    file(REMOVE ${CERR})
+    string(REPLACE ";" " " CMD_STR "${CMD}")
+    message(SEND_ERROR
 "The command
   ${CMD_STR} > ${CERR}
 ended with the error code ${error_result},
@@ -34,4 +38,5 @@ ${output}
 and the following error output:
 ${err}"
 )
+  endif()
 endif()