Following up on #2496. We already have a make themes target. ~Critically, this re-uses the docs/ env for the DocumenterTools dependency.~ Actually, let's use the test/themes environment as before, but let's just move that whole thing to assets/html, so that everything is in one place.
Note: it looks like the new CSS files are actually outdated, at least when building with this.
FWIW, it looks like it was the border changes that didn't get updated. Not the easiest thing to find, but this is where the diff seems to have started diverging:
Following up on #2496. We already have a
make themes
target. ~Critically, this re-uses thedocs/
env for the DocumenterTools dependency.~ Actually, let's use thetest/themes
environment as before, but let's just move that whole thing toassets/html
, so that everything is in one place.Note: it looks like the new CSS files are actually outdated, at least when building with this.