diff options
| author |  David Adam (zanchey) <zanchey@ucc.gu.uwa.edu.au> | 2012-06-18 00:29:11 +0800 |
|---|---|---|
| committer |  ridiculousfish <corydoras@ridiculousfish.com> | 2012-06-17 15:04:20 -0700 |
| commit | 6681f3bfec4d944a9e978aa7d5fd84363ca38cba (patch) | |
| tree | 399462a6bbbb6f56979d7ed45fd8f7a93f731848 /Makefile.in | |
| parent | 71f8960ef1d69e18ebe1485889cf7a880a2db831 (diff) | |
only touch user_doc if doxygen installed
If doxygen isn't installed, an empty file called user_doc will be created.
If doxygen is later installed, the documentation will not generate correctly.
Diffstat (limited to 'Makefile.in')
| -rw-r--r-- | Makefile.in | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/Makefile.in b/Makefile.in index d1f880f4..b70dd621 100644 --- a/Makefile.in +++ b/Makefile.in @@ -337,8 +337,7 @@ prof: user_doc: $(HDR_FILES_SRC) Doxyfile.user user_doc.head.html $(HELP_SRC) $(MAKE) doc.h $(HDR_FILES) - - doxygen Doxyfile.user - touch user_doc + - doxygen Doxyfile.user && touch user_doc # |