# HG changeset patch # User wenzelm # Date 1011908504 -3600 # Node ID 0fce95478e1985377cc34e86fb3bd1ac941b9702 # Parent 66aaa0eb9069d4b07637a9378e7253509ee3cefb copy_styles replaces overly conservative update_styles; diff -r 66aaa0eb9069 -r 0fce95478e19 lib/Tools/latex --- a/lib/Tools/latex Thu Jan 24 18:22:01 2002 +0100 +++ b/lib/Tools/latex Thu Jan 24 22:41:44 2002 +0100 @@ -78,18 +78,7 @@ function run_bibtex () { $ISABELLE_BIBTEX