# HG changeset patch
# User wenzelm
# Date 1625135682 -7200
# Node ID c678e58cf9995580028fb56e5bea4f1e5a14287d
# Parent  1d0d9772fff06983bf727ea3295a662cf5762153
back to scala-2.13.5: avoid problems with history in scala REPL;

diff -r 1d0d9772fff0 -r c678e58cf999 Admin/components/main
--- a/Admin/components/main	Wed Jun 30 22:14:27 2021 +0200
+++ b/Admin/components/main	Thu Jul 01 12:34:42 2021 +0200
@@ -18,7 +18,7 @@
 opam-2.0.7
 polyml-5.8.2
 postgresql-42.2.18
-scala-2.13.6
+scala-2.13.5
 smbc-0.4.1
 spass-3.8ds-2
 sqlite-jdbc-3.34.0
diff -r 1d0d9772fff0 -r c678e58cf999 src/Pure/ROOT.scala
--- a/src/Pure/ROOT.scala	Wed Jun 30 22:14:27 2021 +0200
+++ b/src/Pure/ROOT.scala	Thu Jul 01 12:34:42 2021 +0200
@@ -21,4 +21,3 @@
   val proper_string = Library.proper_string _
   def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list)
 }
-