git.iko.soy/Idris-dev
on master help sign in
Updated test idrisdoc006 to give more information usable on failure.
commit373d40c3e175857cf362c989f07e7c4038f27270 authorPhilip Rasmussen <pjor@itu.dk> dateWed 30 Apr 2014, 15:21 (13 years ago) parentcd92ae8
2 files changed+4−1
compare with master
unifiedsplit
test/idrisdoc006/expected+1 test/idrisdoc006/run+3−1
test/idrisdoc006/expected+1
@@ -1,4 +1,5 @@
11Type checking ./A.idr
2+IdrisDoc file written
23Type checking ./B.idr
34A: Check
45B: Check
test/idrisdoc006/run+3−1
@@ -1,6 +1,8 @@
11#!/usr/bin/env bash
2−# Tests that documentation properly is merged with existing
2+# Tests that documentation properly is merged with existent
3+# Also tests that an IdrisDoc is written
34idris --mkdoc package_a.ipkg
5+[ -f test_merge_doc/IdrisDoc ] && echo "IdrisDoc file written"
46idris --mkdoc package_b.ipkg
57[ -f test_merge_doc/docs/A.html ] && echo "A: Check"
68[ -f test_merge_doc/docs/B.html ] && echo "B: Check"