Works really nicely. Two things: - Formatting issues: http://i.imgur.com/AUy53Oj.png - I don't like the placement. How about we place it in the navigation bar at the top? There is enough space.
On Thu, Apr 2, 2015 at 11:49 AM, Ufuk Celebi <u...@apache.org> wrote: > OK, I've added the change as PRs. Nothing fancy. Would be still nice if > someone checked it out locally and make sure that the search results refer > to the correct doc version. > > https://github.com/apache/flink/pull/563 > https://github.com/apache/flink/pull/564 > > – Ufuk