From 738336e99f5770f6bd39343fcfca5d0e89c16565 Mon Sep 17 00:00:00 2001
From: Raphael Jolly <rjolly@users.sourceforge.net>
Date: Sun, 26 Jul 2020 13:06:06 +0200
Subject: [PATCH] empty

---
 init.js | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/init.js b/init.js
index de411a8..6d3e4db 100644
--- a/init.js
+++ b/init.js
@@ -405,7 +405,7 @@ function classpath() {
     return java.lang.System.getProperty("java.class.path");
 }
 
-// requires ch.epfl.lamp#dotty-compiler_0.22;0.22.0-RC1
+// requires ch.epfl.lamp#dotty-compiler_0.25;0.25.0-RC2
 
 function dotc(srcDir, destDir, options) {
     if (srcDir == undefined) {