mirror of
https://github.com/jenkinsci/jenkins.git
synced 2026-11-13 20:12:14 +00:00
Improve WebSocket Provider interface (#7915)
Improve `Provider` interface
This commit is contained in:
1 parent
264270de59
commit
ac2fc84a9a
3 files changed
+5
-4
No files matched your search
@@ -69,7 +69,8 @@ public abstract class WebSocketSession {
|
||||
if (PING_INTERVAL_SECONDS != 0) {
|
||||
pings = Timer.get().scheduleAtFixedRate(() -> {
|
||||
try {
|
||||
handler.sendPing(ByteBuffer.wrap(new byte[0]));
|
||||
Future<Void> f = handler.sendPing(ByteBuffer.wrap(new byte[0]));
|
||||
// TODO do something interesting with the future
|
||||
} catch (Exception x) {
|
||||
error(x);
|
||||
pings.cancel(true);
|
||||
|
||||
Reference in new issue
Block a user