fixes #1895

usethesource · Nov 29, 2023 · 7687359 · 7687359
1 parent d85f086
commit 7687359
Showing 1 changed file with 7 additions and 7 deletions.
diff --git a/src/org/rascalmpl/library/Prelude.java b/src/org/rascalmpl/library/Prelude.java
@@ -923,15 +923,15 @@ public void iprint(IValue arg, IInteger lineLimit){
 	        // ignore, it's what we wanted
 	    }
 		catch (IOException e) {
-			RuntimeExceptionFactory.io(values.string("Could not print indented value"));
+			throw RuntimeExceptionFactory.io(values.string("Could not print indented value"));
 		}
 		finally {
-		    try {
-		        output.flush();
-		        output.close();
-		    }
-		    catch (IOException e) {
-		    }
+			try {
+				output.flush();
+			}
+			catch (IOException e) {
+				// ignore
+			}
 		}
 	}