doc-src/fixbookmarks

--- a/doc-src/fixbookmarks	Mon Aug 27 17:24:01 2012 +0200
+++ b/doc-src/fixbookmarks	Mon Aug 27 20:19:09 2012 +0200
@@ -1,5 +1,3 @@
-#!/usr/bin/env perl -pi
+#!/bin/bash
 
-s/\\([a-zA-Z]+)\s*/$1/g;
-s/\$//g;
-s/^BOOKMARK/\\BOOKMARK/g;
+perl -pi -e 's/\\([a-zA-Z]+)\s*/$1/g; s/\$//g; s/^BOOKMARK/\\BOOKMARK/g;' "$@"