[#3731] Fix make-devel.sh

diff --git a/doc/devel/make-devel.sh.in b/doc/devel/make-devel.sh.in
index db9d02c7e4f4df65da0af48d5ccdc88e08a7218d..e2c8eddee2f7aa9afa2457894439aac3210f9091 100755 (executable)
--- a/doc/devel/make-devel.sh.in
+++ b/doc/devel/make-devel.sh.in
@@ -2,9 +2,9 @@
 
 set -euv
 
-cd "@builddir@"
+cd '@srcdir@'
 
-mkdir -p html
+mkdir -p '@builddir@/html'
 
-(cat "@srcdir@/Doxyfile"; echo PROJECT_NUMBER=@PACKAGE_VERSION@) | doxygen - > html/doxygen.log 2> html/doxygen-error.log
-echo "$(grep -c ': warning:' html/doxygen-error.log)" warnings/errors detected.
+(cat '@srcdir@/Doxyfile'; echo PROJECT_NUMBER=@PACKAGE_VERSION@) | doxygen - > '@builddir@/html/doxygen.log' 2> '@builddir@/html/doxygen-error.log'
+echo "$(grep -c ': warning:' '@builddir@/html/doxygen-error.log')" warnings/errors detected.