src/Tools/jEdit/src/jedit_resources.scala
changeset 71500 a3ed1b0a132f
parent 70718 5bb025e24224
child 71601 97ccf48c2f0c
equal deleted inserted replaced
71499:29f37eb9bd0f 71500:a3ed1b0a132f