grep: remove "redundant" info page
authorJohn Marino <draco@marino.st>
Fri, 3 Apr 2015 08:26:46 +0000 (10:26 +0200)
committerJohn Marino <draco@marino.st>
Fri, 3 Apr 2015 09:25:05 +0000 (11:25 +0200)
commit5e07a4912e05f5c51b5732644bb9fca3f6ca086d
treeb42e434978f04baecd966d80ca1d7c586a85b201
parent8ced402e1fa55baf628766ca8fadf4e9682e8931
grep: remove "redundant" info page

Grep already has an adequate man page, so we can remove info page without
losing much.
Makefile_upgrade.inc
gnu/usr.bin/grep/Makefile
gnu/usr.bin/grep/doc/Makefile [deleted file]