lib/Tools/latex
changeset 40893 7d88ebdce380
parent 29143 72c960b2b83e
child 48515 3e17f343deb5
--- a/lib/Tools/latex	Thu Dec 02 21:23:56 2010 +0100
+++ b/lib/Tools/latex	Thu Dec 02 23:09:54 2010 +0100
@@ -88,7 +88,7 @@
 function extract_syms ()
 {
   perl -n \
-    -e '(!m,%requires, || m,%requires latin1, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \
+    -e '(!m,%requires, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \
     "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > "$DIR/syms.lst"
   perl -n \
     -e 'm,\\newcommand\{\\isactrl(\w+)\}, && print "$1\n";' \