medInria/medInria-public — pull request #205 by ocommowi (2014-12-12 14:54:09+00:00)
Title: Filter menu navigator

This pull request solves a long running bug in the filter toolbox of the browser area. In addition, it tries to add a filter menu in the workspaces navigator. The problem being, that it is probably too large for that small column...