src/Doc/fixbookmarks
author haftmann
Thu, 23 Nov 2017 17:03:27 +0000
changeset 67087 733017b19de9
parent 53498 05313b45a5ae
permissions -rwxr-xr-x
generalized more lemmas

#!/usr/bin/env bash

perl -pi -e 's/\\([a-zA-Z]+)\s*/$1/g; s/\$//g; s/^BOOKMARK/\\BOOKMARK/g;' "$@"