Thanks for catching that. Rather than try to maintain that number it's
probably better just to remove it, plus spruce up some of the other old
cruft I found in the neighborhood. I installed the attached.
>From bd6f30413f67987ff8260debcd0b52b07e0d5710 Mon Sep 17 00:00:00 2001
From: Paul Eggert
Da
The size of the grep repository is out of date.
|#> git clone git://git.sv.gnu.org/grep
|#> du -bs grep
4670595 grep
|#> cd grep && ./bootstrap && cd ..
|#> du -bs grep
89227609grep
;;;
From 76ac2086bdec8e0aeee
