From 768735948ca09b69226c28c37235a0cc5ff059eb Mon Sep 17 00:00:00 2001 From: "Jurgen J. Vinju" Date: Wed, 29 Nov 2023 14:15:46 +0100 Subject: [PATCH] fixes #1895 --- src/org/rascalmpl/library/Prelude.java | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/org/rascalmpl/library/Prelude.java b/src/org/rascalmpl/library/Prelude.java index 7e559004339..999ee0f41a0 100644 --- 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 + } } }