diff options
author | stobies <unknown> | 2011-12-08 14:46:39 +0100 |
---|---|---|
committer | stobies <unknown> | 2011-12-08 14:46:39 +0100 |
commit | 5caf985ba77219ac6a5e93697d047c0a0d75a1e7 (patch) | |
tree | 8e5200010f042ed9a9d760d20d62791dc623fda9 | |
parent | f520377755e2e3d452dc93b26483dfdf8db716bc (diff) |
Bring SourceView to front when double-clicking source line
-rw-r--r-- | Source/ModelViewer/Main.cs | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs index e4dd3e46..2e612aa1 100644 --- a/Source/ModelViewer/Main.cs +++ b/Source/ModelViewer/Main.cs @@ -658,6 +658,7 @@ namespace Microsoft.Boogie.ModelViewer }
sourceView.largeFont = largeFontToolStripMenuItem.Checked;
sourceView.SetSourceLocation(r);
+ sourceView.BringToFront();
}
}
}
|