idris-lang/Idris-dev — pull request #1103 by PhilipRasmussen (2014-04-23 08:23:35+00:00)
Title: IdrisDoc tests + bug fix

This is tests for IdrisDoc as promised earlier.
While writing them I found a bug related to merging documentations, which I fixed while at it.

Since #1098 the run_backup files have been removed, and the tests have been converted to pure bash scripts to eliminate dependency problems with the added benefit of running faster.
In #1100, #1101 and #1102 the idrisdoc007 test has succeeded locally, but failed when run by Travis. This is a fourth attempt to get the test to work also on the test server.

If someone has a better way of dealing with this issue (tests working locally, but not when pushed), I would like to hear. I think it is rather embarrassing that I have to create so many pull requests for the same merge, and that they keep failing.