elpi icon indicating copy to clipboard operation
elpi copied to clipboard

Published 20 hours ago • verified publisher icon LPCIC

Feature documentation

Open jwintz opened this issue 2 years ago • 4 comments

Test with:

make doc-build

Review doc in docs/build/html

make doc-publish

Review doc in local branch gh-pages

If ok, uncomment pushing in root's Makefile target doc-publish, the release target should then be ok.

jwintz avatar Jun 26 '22 20:06 jwintz

something went wrong with the merge of master in this branch. In master I moved the elpi-trace-elaborator to src/ (but after the merge it is both in ./ and src/ and dune complains). do you want me to fix that?

gares avatar Jun 27 '22 08:06 gares

The old branch is at feature/docold. I did rebase this one and force pushed.

gares avatar Jun 27 '22 08:06 gares

something went wrong with the merge of master in this branch. In master I moved the elpi-trace-elaborator to src/ (but after the merge it is both in ./ and src/ and dune complains). do you want me to fix that?

Yes, would love to.

jwintz avatar Jun 27 '22 10:06 jwintz

The old branch is at feature/docold. I did rebase this one and force pushed.

Fine to me !

jwintz avatar Jun 27 '22 10:06 jwintz