# HG changeset patch
# User wenzelm
# Date 1379776706 -7200
# Node ID 729a43c36ccbbd2c1582175925af9505fe9fc5f4
# Parent  36703fcea740013131d1fc95bc4a57f95fc30aca
proper text replacement (cf. 747835eb2782);

diff -r 36703fcea740 -r 729a43c36ccb lib/Tools/logo
--- a/lib/Tools/logo	Sat Sep 21 17:08:47 2013 +0200
+++ b/lib/Tools/logo	Sat Sep 21 17:18:26 2013 +0200
@@ -80,7 +80,7 @@
 esac
 
 [ -z "$QUIET" ] && echo "${OUTPUT_NAME}.eps" >&2
-perl -p -e "s,<any>,$NAME," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "${OUTPUT_NAME}.eps"
+perl -p -e "s,<any>,$TEXT," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "${OUTPUT_NAME}.eps"
 
 [ -z "$QUIET" ] && echo "${OUTPUT_NAME}.pdf" >&2
 "$ISABELLE_EPSTOPDF" "${OUTPUT_NAME}.eps"