Sat, 16 Dec 2017 15:11:19 +0100 | wenzelm | more operations; | changeset | files |
Sat, 16 Dec 2017 14:40:21 +0100 | wenzelm | tuned; | changeset | files |
Sat, 16 Dec 2017 14:24:12 +0100 | wenzelm | recovered Options.default_markup, e.g. for src/Doc/antiquote_setup.ML (amending 16519cd83ed4); | changeset | files |