Add dependency of userdoc-html to userdoc-pdf

Unfortunately, CMake does allow to specify serial build for some
targets (for all generators).

This fake dependency is used to avoid race conditions that may occur
in building these two targets in parallel (temporary files are
generated during doc generation).

The bad consequence of this change is that one cannot build html doc
without pdf doc if it can be generated...

cmake/PugsDoc.cmake

@@ -99,16 +99,10 @@ if (EMACS AND GNUPLOT_FOUND AND GMSH)
       FILE_PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE
       @ONLY)
 
-    # set_source_files_properties(
-    #   ${PUGS_BINARY_DIR}/build-pdf.sh2
-    #   PROPERTIES
-    #   GENERATED TRUE
-    #   HEADER_FILE_ONLY TRUE
-    # )
-
     add_custom_target(userdoc-pdf DEPENDS pugsdoc-dir "${PUGS_BINARY_DIR}/doc/userdoc.pdf" "${PUGS_BINARY_DIR}/doc/build-userdoc-pdf.sh")
 
     add_dependencies(userdoc userdoc-pdf)
+    add_dependencies(userdoc-html userdoc-pdf)
 
   else()
     if (NOT LATEX_PDFLATEX_FOUND)