diff options
Diffstat (limited to 'documentation/make_header')
| -rwxr-xr-x | documentation/make_header | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/documentation/make_header b/documentation/make_header index a8909b85a..58df10af2 100755 --- a/documentation/make_header +++ b/documentation/make_header @@ -48,7 +48,7 @@ fi # with our PDF document title page (LaTeX code) and write the # result to $DOXY_HEAD. -$DOXY_CMD -w latex $DOXY_TEMP /dev/null /dev/null +"$DOXY_CMD" -w latex $DOXY_TEMP /dev/null /dev/null # combine three parts of these files to the output file # using '( ... ) > $DOXY_HEAD' to write (concatenate) |