David Lechner afba297c41 doc/ide: hide the "view source" link ...

Since these are meant to be offline docs and use a smaller screen area
we can omit this to keep things cleaner.

2021-01-25 20:24:46 -06:00

..

ide.css

doc/ide: hide the "view source" link

2021-01-25 20:24:46 -06:00

theme_overrides.css

doc: override external link style on figure target

2021-01-24 19:58:46 -06:00