Fix unclosed resource warnings
Change-Id: I9beec3e933a9973c216e9b8c4c1b33f9b1dd812e
diff --git a/src/builtin/PRED_close_2.java b/src/builtin/PRED_close_2.java
index 9bba807..9414135 100644
--- a/src/builtin/PRED_close_2.java
+++ b/src/builtin/PRED_close_2.java
@@ -100,12 +100,16 @@
}
} else if (stream instanceof PrintWriter) {
PrintWriter out = (PrintWriter) stream;
- if (out.checkError()) {
- if (! forceFlag)
- throw new SystemException("output stream error");
+ try {
+ if (out.checkError()) {
+ if (! forceFlag) {
+ throw new SystemException("output stream error");
+ }
+ }
+ } finally {
+ out.flush();
+ out.close();
}
- out.flush();
- out.close();
} else {
throw new IllegalDomainException(this, 1, "stream_or_alias", a1);
}
diff --git a/src/builtin/PRED_get_2.java b/src/builtin/PRED_get_2.java
index 2355d53..1fd55ab 100644
--- a/src/builtin/PRED_get_2.java
+++ b/src/builtin/PRED_get_2.java
@@ -66,6 +66,7 @@
throw new PermissionException(this, "input", "stream", a1, "");
// read a non-blank single character
try {
+ @SuppressWarnings("resource")
PushbackReader in = (PushbackReader) stream;
int c = in.read();
while(Character.isWhitespace((char)c))
