Differences

This shows you the differences between two versions of the page.

--- config:start [2023/04/11 10:23]
rajit [Technology-specific configuration]
+++ config:start [2023/06/25 11:13]
rajit [Generic configuration settings]
@@ Line 112: / Line 112: @@
 end
 </code>
+<code>
+begin act
+  int output_window_width 72
+end
+</code>
+For tools that use pretty-printing, this sets the output window width for a line break.