Wed, 21 Nov 2018 15:19:11 +0100 | wenzelm | more robust (see https://code.visualstudio.com/docs/extensionAPI/document-selectors); | changeset | files |
Wed, 21 Nov 2018 14:45:24 +0100 | wenzelm | tuned; | changeset | files |
Wed, 21 Nov 2018 14:33:30 +0100 | wenzelm | more comment markup; | changeset | files |
Tue, 20 Nov 2018 13:46:13 +0100 | wenzelm | tuned -- refining auto-update 15e9ed5b28fb; | changeset | files |
Tue, 20 Nov 2018 13:44:06 +0100 | wenzelm | clarified presentation; | changeset | files |
Mon, 19 Nov 2018 15:32:12 +0100 | nipkow | merged | changeset | files |