restore the page title after escaping out of a search

diff --git a/src/librustdoc/html/static/main.js b/src/librustdoc/html/static/main.js
index b63abec1f0e8b0cc145e27a57bca142d257bddab..70782973e426d2b913d0fe24d54ec97862d19875 100644 (file)
--- a/src/librustdoc/html/static/main.js
+++ b/src/librustdoc/html/static/main.js
@@ -52,6 +52,8 @@
 
     var themesWidth = null;
 
+    var titleBeforeSearch = document.title;
+
     if (!String.prototype.startsWith) {
         String.prototype.startsWith = function(searchString, position) {
             position = position || 0;
@@ -267,6 +269,7 @@
             ev.preventDefault();
             addClass(search, "hidden");
             removeClass(document.getElementById("main"), "hidden");
+            document.title = titleBeforeSearch;
         }
         defocusSearchBar();
     }