Categories
Release Notes: Workbench

Workbench 9.3.1.2

  • 8671: Workbench now respects the “report_output_font_name” GUI property in ~/.method-r/workbench/version/gui.properties.
  • 8668: ERROR lines now populate the $tim, $tim1, and $tim0 mrskew variables.
  • 8637: Fixed a bug causing the command text area not to resize properly when zooming.

Leave a Reply

This site uses Akismet to reduce spam. Learn how your comment data is processed.