Merge pull request #7666 from minrk/edit-download

add download link to editor

IPython/html/static/edit/js/menubar.js

@@ -74,6 +74,11 @@ define([
         this.element.find('#rename-file').click(function () {
             that.save_widget.rename();
         });
+        this.element.find('#download-file').click(function () {
+            window.open(utils.url_join_encode(
+                that.base_url, 'files', that.editor.file_path
+            ) + '?download=1');
+        });
         
         // Edit
         this.element.find('#menu-find').click(function () {

IPython/html/templates/edit.html

@@ -48,6 +48,7 @@ data-file-path="{{file_path}}"
                 <li id="new-file"><a href="#">New</a></li>
                 <li id="save-file"><a href="#">Save</a></li>
                 <li id="rename-file"><a href="#">Rename</a></li>
+                <li id="download-file"><a href="#">Download</a></li>
               </ul>
             </li>
             <li class="dropdown"><a href="#" class="dropdown-toggle" data-toggle="dropdown">Edit</a>