From 5fade71e09fafdf29803035903cf610c93e491a7 Mon Sep 17 00:00:00 2001 From: jprocter Date: Wed, 17 Aug 2011 12:15:36 +0100 Subject: [PATCH] fix for JAL-888 --- src/jalview/gui/WsPreferences.java | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/src/jalview/gui/WsPreferences.java b/src/jalview/gui/WsPreferences.java index ff149c1..e14b358 100644 --- a/src/jalview/gui/WsPreferences.java +++ b/src/jalview/gui/WsPreferences.java @@ -159,6 +159,10 @@ public class WsPreferences extends GWsPreferences { if (old) { + if (oldUrls!=wsUrls || (wsUrls!=null && oldUrls!=null && !wsUrls.equals(oldUrls))) + { + update++; + } wsUrls = (oldUrls == null) ? null : new Vector(oldUrls); } else @@ -419,8 +423,14 @@ public class WsPreferences extends GWsPreferences protected void resetWs_actionPerformed(ActionEvent e) { jalview.ws.jws2.Jws2Discoverer.setServiceUrls(null); - wsUrls = jalview.ws.jws2.Jws2Discoverer.getServiceUrls(); + Vector nwsUrls = jalview.ws.jws2.Jws2Discoverer.getServiceUrls(); + if (!wsUrls.equals(nwsUrls)) { + update++; + } + wsUrls=nwsUrls; updateList(); + + updateAndRefreshWsMenuConfig(true); } protected void ok_ActionPerformed(ActionEvent e) -- 1.7.10.2