From 051b99e441799fe2d1d181aeafb2352fe141e79e Mon Sep 17 00:00:00 2001 From: Raphael Jolly Date: Tue, 13 Oct 2020 22:36:45 +0200 Subject: [PATCH] empty --- init.js | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/init.js b/init.js index 3613455..a2fb1aa 100644 --- a/init.js +++ b/init.js @@ -409,7 +409,7 @@ function classpath() { return java.lang.System.getProperty("java.class.path"); } -// requires ch.epfl.lamp#dotty-compiler_0.25;0.25.0-RC2 +// requires ch.epfl.lamp#dotty-compiler_0.27;0.27.0-RC1 function dotc(srcDir, destDir, options) { if (srcDir == undefined) {