# HG changeset patch
# User wenzelm
# Date 1621346461 -7200
# Node ID aa7662e475b6e309eaf194891e72abd97aedbdce
# Parent  cd9afbd0ccb94b58b1207df0d9746aa69b36e524
obsolete (see 5a3a2a52648d);

diff -r cd9afbd0ccb9 -r aa7662e475b6 lib/Tools/latex
--- a/lib/Tools/latex	Tue May 18 15:57:49 2021 +0200
+++ b/lib/Tools/latex	Tue May 18 16:01:01 2021 +0200
@@ -13,7 +13,7 @@
   echo "Usage: isabelle $PRG [OPTIONS] [FILE]"
   echo
   echo "  Options are:"
-  echo "    -o FORMAT    specify output format: pdf (default), bbl, idx, sty"
+  echo "    -o FORMAT    specify output format: pdf (default), bbl, idx"
   echo
   echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
   echo "  producing the specified output format."
@@ -80,14 +80,6 @@
   return "$RC"
 }
 function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
-function copy_styles ()
-{
-  for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty
-  do
-    TARGET="$DIR"/$(basename "$STYLEFILE")
-    perl -p -e 's/\$[I]d:?(?:\s)*([^\$]*)\$//g' "$STYLEFILE" > "$TARGET"
-  done
-}
 
 case "$OUTFORMAT" in
   pdf)
@@ -105,10 +97,6 @@
     run_makeindex
     RC="$?"
     ;;
-  sty)
-    copy_styles
-    RC="$?"
-    ;;
   *)
     fail "Bad output format '$OUTFORMAT'"
     ;;