--- a/client/js/paper-renderer.js Tue May 28 16:45:12 2013 +0200
+++ b/client/js/paper-renderer.js Thu May 30 12:08:28 2013 +0200
@@ -1913,7 +1913,7 @@
+ '<div class="Rk-TopBar-Separator"></div>'
+ '<% } %></div><% } %>'
+ '<div class="Rk-Editing-Space<% if (!options.show_top_bar) { %> Rk-Editing-Space-Full<% } %>">'
- + '<div class="Rk-Labels"></div><canvas class="Rk-Canvas" resize></canvas><div class="Rk-Editor"><div class="Rk-Notifications"></div>'
+ + '<div class="Rk-Labels"></div><canvas class="Rk-Canvas" resize></canvas><div class="Rk-Notifications"></div><div class="Rk-Editor">'
+ '<% if (options.show_bins) { %><div class="Rk-Fold-Bins">«</div><% } %>'
+ '<div class="Rk-ZoomButtons"><div class="Rk-ZoomIn" title="<%-translate("Zoom In")%>"></div><div class="Rk-ZoomOut" title="<%-translate("Zoom Out")%>"></div></div>'
+ '</div></div>'