Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Attempt to fix
tools/run_doxygen.sh
for travis-ci (part 3)
- previous commit 6f6a058 didn't work - after installing and running travis locally, it seems that `grep` returns a non-zero exit status if nothing matches (i.e., we want nothing to match!) --> use grep ... || echo "" instead
- Loading branch information