Admin/components/optional
author wenzelm
Wed, 15 Jan 2020 19:54:50 +0100
changeset 71383 8313dca6dee9
parent 58842 22b87ab47d3b
child 73647 a037f01aedab
permissions -rw-r--r--
misc tuning, following hint by IntelliJ;

#optional components that could impact build time significantly
hol-light-bundle-0.5-126