proper text replacement (cf. 747835eb2782);

--- 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"