Admin/components/optional
author wenzelm
Sun, 15 Jan 2023 12:55:23 +0100
changeset 76984 29432d4a376d
parent 73647 a037f01aedab
permissions -rw-r--r--
more robust: rely on PIDE markup instead of regex guess;

#optional components: somewhat experimental tools
hol-light-bundle-0.5-126