# HG changeset patch
# User wenzelm
# Date 1543872095 -3600
# Node ID 9e488aeb98709a852dee63d8461524f3155cf29a
# Parent  0698ded5caf14962594abb813435f247e82c6fca
updated to jedit_build-20181203 (according to d70767e508d7);

diff -r 0698ded5caf1 -r 9e488aeb9870 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Mon Dec 03 22:07:23 2018 +0100
+++ b/Admin/components/components.sha1	Mon Dec 03 22:21:35 2018 +0100
@@ -138,6 +138,7 @@
 23c8a05687d05a6937f7d600ac3aa19e3ce59c9c  jedit_build-20180504.tar.gz
 9c64ee0705e5284b507ca527196081979d689519  jedit_build-20181025.tar.gz
 cfa65bf8720b9b798ffa0986bafbc8437f44f758  jedit_build-20181026.tar.gz
+847492b75b38468268f9ea424d27d53f2d95cef4  jedit_build-20181203.tar.gz
 0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa  jfreechart-1.0.14-1.tar.gz
 8122526f1fc362ddae1a328bdbc2152853186fee  jfreechart-1.0.14.tar.gz
 d911f63a5c9b4c7335bb73f805cb1711ce017a84  jfreechart-1.5.0.tar.gz
diff -r 0698ded5caf1 -r 9e488aeb9870 Admin/components/main
--- a/Admin/components/main	Mon Dec 03 22:07:23 2018 +0100
+++ b/Admin/components/main	Mon Dec 03 22:21:35 2018 +0100
@@ -6,7 +6,7 @@
 e-2.0-2
 isabelle_fonts-20181129
 jdk-11+28
-jedit_build-20181026
+jedit_build-20181203
 jfreechart-1.5.0
 jortho-1.0-2
 kodkodi-1.5.2-1