| commit | 1d75766c7f805c5eac001a2eebc07588b303e3a5 | [log] [tgz] |
|---|---|---|
| author | eyuen <eyuen> | Wed Apr 11 22:09:28 2012 +0000 |
| committer | eyuen <eyuen> | Wed Apr 11 22:09:28 2012 +0000 |
| tree | 886b0022e5ae057298f7136a6018d28d98b2423b | |
| parent | 8384104003da7caa3ab55e6a43d4d84ea297e7cf [diff] |
[375507] deleting a server with a dirty server editor
diff --git a/plugins/org.eclipse.wst.server.ui/serverui/org/eclipse/wst/server/ui/internal/editor/ServerEditor.java b/plugins/org.eclipse.wst.server.ui/serverui/org/eclipse/wst/server/ui/internal/editor/ServerEditor.java index 5f38ef9..f9723a1 100644 --- a/plugins/org.eclipse.wst.server.ui/serverui/org/eclipse/wst/server/ui/internal/editor/ServerEditor.java +++ b/plugins/org.eclipse.wst.server.ui/serverui/org/eclipse/wst/server/ui/internal/editor/ServerEditor.java
@@ -95,8 +95,12 @@ // do nothing } public void serverRemoved(IServer oldServer) { - if (oldServer.equals(server.getOriginal()) && !isDirty()) - closeEditor(); + if (oldServer.equals(server.getOriginal())) { + resourceDeleted = true; + if (!isDirty()) { + closeEditor(); + } + } } }