You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
It's not possible to reference a package main page, which is not a special concept in Odoc but currently a regular page (#1037).
Drivers currently change the name of the index.mld page and there's no conventional name (Dune names it <package name>.odoc but Voodoo names it <version string>.odoc).
This might also be used to write unambiguous fully-qualified references in the future (eg. package_name.library.Module).
The text was updated successfully, but these errors were encountered:
It's not possible to reference a package main page, which is not a special concept in Odoc but currently a regular page (#1037).
Drivers currently change the name of the
index.mld
page and there's no conventional name (Dune names it<package name>.odoc
but Voodoo names it<version string>.odoc
).This might also be used to write unambiguous fully-qualified references in the future (eg.
package_name.library.Module
).The text was updated successfully, but these errors were encountered: