idris-lang/Idris-dev — pull request #1101 by PhilipRasmussen (2014-04-23 00:52:07+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.
Since #1100 a broken test has been fixed. It depended on an empty directory which git happily did ignore.

Hopefully everything will be perfectly fine this time.