Skip to content

Instantly share code, notes, and snippets.

@rgrinberg

rgrinberg/*compilation*.txt

Created July 11, 2017 17:43
Show Gist options
  • Save rgrinberg/e2853172a2012580392578ae82620115 to your computer and use it in GitHub Desktop.
Save rgrinberg/e2853172a2012580392578ae82620115 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
*compilation*.txt
(rule (with-stdout-to html_sigs.ml
(progn
(echo "[@@@warning \"-a\"]\nmodule rec HACK : sig\n")
(cat html_sigs.mli)
(echo "\nend = HACK\ninclude HACK\n"))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment