JuliaLang/julia — pull request #1417 by vtjnash (2012-10-20 23:42:19+00:00)
Title: add scrollbar to html docs sidebar

Adds a scrollbar to the html documentation sidebar, when necessary, to the left of the closure button bar. Otherwise, I tried to keep the style unchanged.

It's possible to easily make the following additional changes, if desired, separately or together:
1) Always pin the box to the top of the window. (comment out line 170 `sidebar.css('top', Math.max(bodyoff,0));`)

2) Full height expansion of sidebar to available height (requires a tweak to background-color in css, and the removal of a few lines of javascript)