src/Doc/fixbookmarks
author wenzelm
Wed, 31 Oct 2018 15:53:32 +0100
changeset 69216 1a52baa70aed
parent 53498 05313b45a5ae
permissions -rwxr-xr-x
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);

#!/usr/bin/env bash

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