diff -r 7f3760f39bdc -r f8845fc8f38d doc-isac/jrocnik/fixbookmarks.pl
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-isac/jrocnik/fixbookmarks.pl	Tue Sep 17 09:50:52 2013 +0200
@@ -0,0 +1,4 @@
+
+s/\\([a-zA-Z]+)\s*/$1/g;
+s/\$//g;
+s/^BOOKMARK/\\BOOKMARK/g;