updated to jedit_build-20190224 (new patches: favorites, glyphvector);
authorwenzelm
Sun, 24 Feb 2019 13:00:43 +0100
changeset 69840 a35033167f01
parent 69839 828f3cd0dcf9
child 69841 b3c9291b5fc7
updated to jedit_build-20190224 (new patches: favorites, glyphvector);
Admin/components/components.sha1
Admin/components/main
--- 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
--- 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