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 |
Sat, 16 Dec 2017 12:28:46 +0100 | wenzelm | tuned; | changeset | files |
Sat, 16 Dec 2017 12:27:10 +0100 | wenzelm | clarified signature; | changeset | files |