Add buttons to jump to next/prev outputmark in an outputwidget.
I added buttons to all output widgets instead of the one for the build tool view; we can easily restrict this to a certain type of view if we want to. The only problem with the buttons is that they are enabled even if there are no outputmarks to jump to. At the time of creating this diff, I did not see an easy way to find the number of outputmark. REVIEW: 115600 BUG: 330206
parent
4fd7b16f
Please register or sign in to comment