git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/test/idrisdoc007/run
6 lines 207 B history raw
1#!/usr/bin/env bash
2# Tests that documentation only is written when safe
3mkdir do_not_delete_doc
4idris --mkdoc package.ipkg > nowhere
5echo Exit status \(expects 1\): $?
6rm -rf do_not_delete_doc *.ibc nowhere