diff --git a/doxygen.sh a/doxygen.sh
new file mode 100755
index 0000000000..1a2485251c
--- /dev/null
+++ a/doxygen.sh
@@ -0,0 +1 @@
+#!/bin/sh