Zachary Yedidia 423f4675d2 Add a scroll bar option ...

The option is `scrollbar` and is off by default. The scroll bar is
not interactive (you can't click and drag it) but this will likely
be fixed in the future.

Ref #869

2017-11-05 20:07:14 -05:00

..

micro

Add a scroll bar option

2017-11-05 20:07:14 -05:00