# HG changeset patch
# User wenzelm
# Date 1346091549 -7200
# Node ID f0d87c6b7a2e1d9ab53e0457eb190b2907f1024c
# Parent  83bd9eb1c70ca2f0aac73750111fcc68b2730efd
more portable perl invocation;

diff -r 83bd9eb1c70c -r f0d87c6b7a2e 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;' "$@"