mn200/HOL — pull request #183 by ptroja (2014-08-01 23:34:37+00:00)
Title: Minor fixes to "DESCRIPTION" manual

Fixes to some minor, mostly typographic issues.

mn200: You can revert or ignore the "/bin/rm -> rm" commit; I messed up my git repo. Sorry.