diff options
| author | davemds <dave@gurumeditation.it> | 2014-02-08 21:32:02 +0100 |
|---|---|---|
| committer | davemds <dave@gurumeditation.it> | 2014-02-08 21:32:02 +0100 |
| commit | 3a6aed8017dbb2dc60df71b45e5e62c26a929ebb (patch) | |
| tree | 4d5d8f257eba3c51bde19a23d2a7b95f7470d32e /configure.ac | |
| parent | d7c68722e26069ece8caf6659fb8f24d15df7084 (diff) | |
Show docs info/instructions in config summary
Diffstat (limited to 'configure.ac')
| -rw-r--r-- | configure.ac | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/configure.ac b/configure.ac index e7e61808e..72e1c47e4 100644 --- a/configure.ac +++ b/configure.ac | |||
| @@ -767,6 +767,11 @@ echo "Tests......................: no" | |||
| 767 | else | 767 | else |
| 768 | echo "Tests......................: make check" | 768 | echo "Tests......................: make check" |
| 769 | fi | 769 | fi |
| 770 | if test "${build_doc}" = "no"; then | ||
| 771 | echo "Docs.......................: no (doxygen not found)" | ||
| 772 | else | ||
| 773 | echo "Docs.......................: make doc" | ||
| 774 | fi | ||
| 770 | echo | 775 | echo |
| 771 | echo "Installation...............: make install (as root if needed, with 'su' or 'sudo')" | 776 | echo "Installation...............: make install (as root if needed, with 'su' or 'sudo')" |
| 772 | echo " prefix...................: $prefix" | 777 | echo " prefix...................: $prefix" |