Index: webkit/glue/devtools/js/devtools.js |
=================================================================== |
--- webkit/glue/devtools/js/devtools.js (revision 19806) |
+++ webkit/glue/devtools/js/devtools.js (working copy) |
@@ -110,24 +110,21 @@ |
/** |
* @param {string} url Url frame navigated to. |
- * @param {bool} topLevel True iff top level navigation occurred. |
* @see tools_agent.h |
* @private |
*/ |
-devtools.ToolsAgent.prototype.frameNavigate_ = function(url, topLevel) { |
- if (topLevel) { |
- this.reset(); |
- // Do not reset Profiles panel. |
- var profiles = null; |
- if ('profiles' in WebInspector.panels) { |
- profiles = WebInspector.panels['profiles']; |
- delete WebInspector.panels['profiles']; |
- } |
- WebInspector.reset(); |
- if (profiles != null) { |
- WebInspector.panels['profiles'] = profiles; |
- } |
+devtools.ToolsAgent.prototype.frameNavigate_ = function(url) { |
+ this.reset(); |
+ // Do not reset Profiles panel. |
+ var profiles = null; |
+ if ('profiles' in WebInspector.panels) { |
+ profiles = WebInspector.panels['profiles']; |
+ delete WebInspector.panels['profiles']; |
} |
+ WebInspector.reset(); |
+ if (profiles != null) { |
+ WebInspector.panels['profiles'] = profiles; |
+ } |
}; |