1 files changed, 15 insertions, 0 deletions
diff --git a/doc/buildexamplelist.sh b/doc/buildexamplelist.sh
new file mode 100755
index 000000000..0a9bb7ec0
--- /dev/null
+++ b/doc/buildexamplelist.sh
@@ -0,0 +1,15 @@
+#!/bin/sh
+
+echo "namespace Eigen {"
+echo "/** \page ExampleList"
+echo "<h1>Selected list of examples</h1>"
+
+grep \\addexample $1/Eigen/* -R | cut -d \\ -f 2- | \
+while read example;
+do
+anchor=`echo "$example" | cut -d " " -f 2`
+text=`echo "$example" | cut -d " " -f 4-`
+echo "\\\li \\\ref $anchor \"$text\""
+done
+echo "*/"
+echo "}"
+\ No newline at end of file