coqdocjs icon indicating copy to clipboard operation
coqdocjs copied to clipboard

Using coqdoc's libname

Open motrellin opened this issue 1 year ago • 0 comments

I currently use the coqdoc-option --lib-name <string> to combine several packages in one project under one name. For example, this can be seen here. After trying around a bit with coqdocjs, I want to include the style to some of my projects. Unfortunately, it seems like such libnames are not shown at the html-output. Is there a way to make them visible in a nice way?

motrellin avatar Apr 09 '24 23:04 motrellin