Convert manual from Wiki to mld #951
Merged
Commits on Apr 15, 2024
-
Convert manual from Wiki to mld
This allows to view the manual offline. Converted with: sed -E \ -e 's/^==== *(.*) *====/{3 \1}/g' \ -e 's/^=== *(.*) *===/{2 \1}/g' \ -e 's/^== *(.*) *==/{1 \1}/g' \ -e 's/^= *(.*) *=/{0 \1}/g' \ -e 's/\[\[(.*)\|(.*)]]/{{: \1 }\2}/g' \ -e 's|//(.*)//|{e \1}|g' \ -e 's/<<a_api text=".*" *\| module (.+)>>/in {!\1}/g' \ -e 's/<<code language="ocaml" *\|/{[\n/g' \ -e 's/<<code language="c" *\|/{@c[/g' \ -e 's/>>/]}/g' \ -e "s/\`\`(.*)''/“\1”/g" \ -e 's/\.\.\./…/g' \ "$@" | \ perl -pe 's|{{{(.*?)}}}|[\1]|g' and then some manual fixes for lists and tables. -
-
-
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.