search

digraphs / Digraphs

The GAP package Digraphs
https://digraphs.github.io/Digraphs
Other
30 stars 44 forks source link

Add custom CSS to documentation #640

Closed mtorpey closed 5 months ago

mtorpey commented 5 months ago

It may be useful to have our own custom CSS in the HTML version of manual, as recently when adding images in figures. There's some system for this in GAPDoc, but it appears to be for adding user-choosable styles that can be turned on and off, which isn't quite what we want. Here, we simply append some custom css to GAPDoc's main manual.css file after copying it to the directory, which the GAPDoc manual at least says we're allowed to do.

This can hopefully avoid hacky non-semantic HTML we might be tempted to write in the future.

james-d-mitchell commented 5 months ago

Nice one @mtorpey, I've enabled auto-merge so if the CI passes this'll be merged.