Ticket #21415: patch-doc-tools-latex_filter.diff

File patch-doc-tools-latex_filter.diff, 340 bytes (added by kiyoshi.coquser@…, 15 years ago)

latex_filter patch

  • doc/tools/latex_filter

    old new  
    1212while : ; do
    1313  read -r line;
    1414  case $line in
     15    "! pdfTeX warning (dest)"*)
     16      verbose=0
     17      echo $line $chapter;
     18      ;;
    1519    "! "*)
    1620      echo $line $file;
    1721      error=1