# HG changeset patch
# User wenzelm
# Date 1551009643 -3600
# Node ID a35033167f0176ea78485b7afc86aefb98bda74d
# Parent  828f3cd0dcf95cecaf5439130ae3f116ed02e88b
updated to jedit_build-20190224 (new patches: favorites, glyphvector);

diff -r 828f3cd0dcf9 -r a35033167f01 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Sun Feb 24 12:53:23 2019 +0100
+++ b/Admin/components/components.sha1	Sun Feb 24 13:00:43 2019 +0100
@@ -148,6 +148,7 @@
 847492b75b38468268f9ea424d27d53f2d95cef4  jedit_build-20181203.tar.gz
 536a38ed527115b4bf2545a2137ec57b6ffad718  jedit_build-20190120.tar.gz
 58b9f03e5ec0b85f8123c31f5d8092dae5803773  jedit_build-20190130.tar.gz
+ec0aded5f2655e2de8bc4427106729e797584f2f  jedit_build-20190224.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 828f3cd0dcf9 -r a35033167f01 Admin/components/main
--- a/Admin/components/main	Sun Feb 24 12:53:23 2019 +0100
+++ b/Admin/components/main	Sun Feb 24 13:00:43 2019 +0100
@@ -6,7 +6,7 @@
 e-2.0-2
 isabelle_fonts-20190210
 jdk-11.0.2+9
-jedit_build-20190130
+jedit_build-20190224
 jfreechart-1.5.0
 jortho-1.0-2
 kodkodi-1.5.2-1