Sun, 05 Mar 2017 13:34:35 +0100 | wenzelm | more robust treatment of pending input/output: these are often correlated; | changeset | files |
Sun, 05 Mar 2017 12:07:36 +0100 | nipkow | merged | changeset | files |
Sun, 05 Mar 2017 10:57:51 +0100 | nipkow | added numeral_powr_numeral | changeset | files |
Sat, 04 Mar 2017 22:07:31 +0100 | wenzelm | merged | changeset | files |
Sat, 04 Mar 2017 21:47:26 +0100 | wenzelm | clarified pretty margin; | changeset | files |
Sat, 04 Mar 2017 21:04:44 +0100 | wenzelm | more general hover_message (see also JEdit_Rendering.tooltip_message); | changeset | files |