idris-lang/Idris-dev — pull request #1152 by david-christiansen (2014-05-01 12:41:20+00:00)
Title: Properly ignore comments in ipkg files

Fixes #1149.

This replaces a hacky bad version from yesterday.