Skip to content

Commit ecc0957

Browse files
author
John Nonweiler
committed
Add doxygen version check
Check which version of doxygen is being used in ./scripts/run_doxygen.sh, and add a sentence to the documentation about using the correct version. The warnings produced by doxygen are different for different versions of doxygen, so it is important, when comparing a list of expected warnings, to use the right version of doxygen.
1 parent 43c84f8 commit ecc0957

File tree

2 files changed

+13
-1
lines changed

2 files changed

+13
-1
lines changed

doc/architectural/compilation-and-development.md

+3-1
Original file line numberDiff line numberDiff line change
@@ -197,7 +197,9 @@ The doxygen documentation can be [accessed online](http://cprover.diffblue.com).
197197
To build it locally, run `scripts/run_doxygen.sh`. HTML output will be created
198198
in `doc/html/`. The index page is `doc/html/index.html`. This script will
199199
filter out expected warning messages from doxygen, so that new problems are more
200-
obvious. In the event that any change fixes an old warning, then the
200+
obvious. It is important to use the correct version of doxygen, as specified
201+
in `run_doxygen.sh`, so that there are no unexpected changes to the list of
202+
expected warnings. In the event that any change fixes an old warning, then the
201203
corresponding line(s) should be deleted from
202204
`scripts/expected_doxygen_warnings.txt`. We want to avoid adding any more
203205
warnings to this list of expected warnings, but that can be done to work around

scripts/run_doxygen.sh

+10
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,15 @@
11
#!/bin/bash
22

3+
# Check doxygen version
4+
EXPECTED_VERSION="1.8.14"
5+
doxygen --version | grep -x $EXPECTED_VERSION > /dev/null
6+
if [ $? -ne 0 ]
7+
then
8+
echo "WARNING: Using wrong version of doxygen.\
9+
The list of expected warnings is for version $EXPECTED_VERSION."
10+
fi
11+
12+
# Run doxygen and filter warnings
313
SCRIPT_FOLDER=`dirname $0`
414
cd $SCRIPT_FOLDER/../src
515
doxygen 2>&1 | ../scripts/filter_expected_warnings.py ../scripts/expected_doxygen_warnings.txt

0 commit comments

Comments
 (0)