-
Notifications
You must be signed in to change notification settings - Fork 99
Separate commands for html generation of page+units and implementation #1188
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Conversation
This has never been used and is not the way to go with odoc 3
We don't make the distinction anymore in odoc3. This also removes the --source-root argument.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Awesome! All this code that we didn't need is gone :)
@@ -1,11 +0,0 @@ | |||
open Or_error | |||
|
|||
val compile : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The driver currently did not build source trees but this change means that the driver will have to generate regular pages in the source hierarchy.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think the odoc source tree mechanism is not well suited for generating source pages in the context of odoc 3. If we design a way for odoc to generate the missing pages, it would be different from the one removed here. So I think it is safe to remove it!
Ooh I do like a good cleanup :-) |
Just want to check though: should it be |
Also we should have some negative tests - what happens when you do |
In the odoc dev meeting, we decided to rename it to |
Source is now the positional argument, while impl is passed as an argument. When we generate source for other files (such as dune or .mli or Makefiles or ...) this will come handy.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this is ready to be merged :) I've left some comments but I think it's fine to discuss them after this is merged.
This was suggested in #1185 (comment)
The benefit is cleaner man pages, safer CLI validation.
This PR also takes this opportunity to do some cleanup, by removing the old and never used way of rendering sources:
--source-root
option which is not anymore usable in odoc 3.Once this is merged, I'll rebase #1185 on top and apply @Julow's comment!