| author | wenzelm | 
| Sun, 01 Jan 2023 22:54:40 +0100 | |
| changeset 76858 | 39db5e268aaf | 
| parent 73653 | d9823224fcfe | 
| child 81297 | 07f64697408e | 
| permissions | -rw-r--r-- | 
| 
73653
 
d9823224fcfe
build auxiliary jEdit component in Isabelle/Scala;
 
wenzelm 
parents: 
72247 
diff
changeset
 | 
1  | 
diff -ru jedit5.6.0/jEdit/org/jedit/localization/jedit_en.props jedit5.6.0-patched/jEdit/org/jedit/localization/jedit_en.props  | 
| 
 
d9823224fcfe
build auxiliary jEdit component in Isabelle/Scala;
 
wenzelm 
parents: 
72247 
diff
changeset
 | 
2  | 
--- jedit5.6.0/jEdit/org/jedit/localization/jedit_en.props 2020-09-03 05:31:10.000000000 +0200  | 
| 
 
d9823224fcfe
build auxiliary jEdit component in Isabelle/Scala;
 
wenzelm 
parents: 
72247 
diff
changeset
 | 
3  | 
+++ jedit5.6.0-patched/jEdit/org/jedit/localization/jedit_en.props 2021-05-10 11:02:05.788257753 +0200  | 
| 
71932
 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 
wenzelm 
parents: 
69838 
diff
changeset
 | 
4  | 
@@ -1277,8 +1277,7 @@  | 
| 65329 | 5  | 
The most likely reason is that the JAR file is corrupt; try\n\  | 
6  | 
reinstalling it. See Utilities->Troubleshooting->Activity Log\n\  | 
|
7  | 
for a full stack trace.  | 
|
8  | 
-plugin-error.start-error=Cannot start: {0}\n\
 | 
|
9  | 
- Try updating to a newer version of the plugin.  | 
|
10  | 
+plugin-error.start-error=Cannot start: {0}
 | 
|
11  | 
plugin-error.already-loaded=Two copies installed. Please remove one of the \  | 
|
12  | 
two copies.  | 
|
13  | 
 plugin-error.dep-jdk=Requires Java {0} or later, but you only have version {1}.
 | 
|
| 
73653
 
d9823224fcfe
build auxiliary jEdit component in Isabelle/Scala;
 
wenzelm 
parents: 
72247 
diff
changeset
 | 
14  | 
Binary files jedit5.6.0/jedit.jar and jedit5.6.0-patched/jedit.jar differ  |