Closed Alizter closed 2 years ago
I have no idea how this works, so I cannot understand the changes to the lines starting with a #
, but I can trust you and merge this. In fact, I can even add you to the @coq/website-maintainers team if you wish.
Well, I only changed yamlpp.mll
but after make it updated yamlpp.ml
which it didn't do before. I therefore commited both. I am also not 100% sure I haven't broken anything, so a review from @coq/website-maintainers would be helpful.
I wouldn't mind joining that team also.
OK, I see, thanks! Unfortunately, I don't think anyone currently has maintenance expertise in this code. We barely touch it until it goes away with a full website rework. On my machine it works fine with the change, so it looks good to go.
I'll add you to the team.
I removed a deprecated namespace in yamlpp.mll and the newly generated yamlpp.ml no longer emits a warning.