Merge branch 'refs/heads/t/rm_source_browser'
authorAndre Noll <maan@tuebingen.mpg.de>
Mon, 19 Dec 2016 17:06:52 +0000 (18:06 +0100)
committerAndre Noll <maan@tuebingen.mpg.de>
Mon, 19 Dec 2016 17:13:01 +0000 (18:13 +0100)
commit904e302f0b64887f18c9e2fec7b0bb405675ad22
tree08be2788fe15dfd1af2898906463d27667dc9b40
parentf80453b693e6d3ce5450755310faf5e5d6e5c143
parent67808e59c9d94d3cf68733e94d4afaa1eecb7e8c
Merge branch 'refs/heads/t/rm_source_browser'

Cooking for five months.

A single patch which gets rid of the source browser generated with
global, reducing the size of the web pages considerably.

* refs/heads/t/rm_source_browser:
  web: Remove extra source browser.
NEWS.md