--- a/src/Pure/General/mailman.scala Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/General/mailman.scala Thu Mar 04 21:04:27 2021 +0100
@@ -55,7 +55,7 @@
Some(path)
}
}
- finally { connection.getInputStream.close }
+ finally { connection.getInputStream.close() }
})
}
}