idris-1.3.3: test/idrisdoc001/run.sh
#!/usr/bin/env bash
# Tests that no documentation is built for empty and/or private-only namespaces
${IDRIS:-idris} $@ --mkdoc test_empty.ipkg
rm -rf *.ibc *_doc
#!/usr/bin/env bash
# Tests that no documentation is built for empty and/or private-only namespaces
${IDRIS:-idris} $@ --mkdoc test_empty.ipkg
rm -rf *.ibc *_doc