- Use '/' key to quickly access this field.
- Enter a name of repository, or repository group for quick search.
- Prefix query to allow special search:
user:admin, to search for usernames, always global
user_group:devops, to search for user groups, always global
pr:303, to search for pull request number, title, or description, always global
commit:efced4, to search for commits, scoped to repositories or groups
file:models.py, to search for file paths, scoped to repositories or groups
For advanced full text search visit: repository search
on resume, print server info again
This commit makes it possible to differentiate between many different
long-running notebook servers, where the original ip address and port
information printed at the beginning has scrolled out of the screen.
We save the server location string that gets printed on startup, and
re-print it when the user attempts to interrupt the server with Ctrl-C
Thanks to @minrk for discussion on how this should work.
Also added a docstring to the start() method
