##// END OF EJS Templates
bookmarks: set the current bookmark to the new name if we rename the current bookmark...
bookmarks: set the current bookmark to the new name if we rename the current bookmark If we rename the current bookmark, we have to set the current bookmark to the new name.

File last commit:

r1360:7d439981 default
r7550:fead6cf9 default
Show More
__init__.py
1 line | 14 B | text/x-python | PythonLexer
# placeholder