diff options
| -rwxr-xr-x | dist/s_docs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dist/s_docs b/dist/s_docs index c84ab5c11a9..77a5ef99a2b 100755 --- a/dist/s_docs +++ b/dist/s_docs @@ -3,7 +3,7 @@ # We require doxygen which may not be installed. type doxygen > /dev/null 2>&1 || { echo 'doxygen not found, skipping document creation' - return 1 + exit 1 } filter= |