Closed fingolfin closed 1 year ago
Before this, make doc would end up in a GAP prompt, which is against any convention and makes it unusable in automation.
make doc
Also omit the GAP banner.
Fixes #100.
Before this,
make doc
would end up in a GAP prompt, which is against any convention and makes it unusable in automation.Also omit the GAP banner.
Fixes #100.