On Sat 30 Jul 2016 at 17:21:47 (-0600), ghe wrote: > I found it, and it was all my doing. > > Some time ago, I built a script that replaced "ping" with "ping.dist > -c 3 $1" (and forgot that I had) so I wouldn't have to type -c 3 all > the time. That broke ping for everybody else.
I think you can have your cake and eat it if you put this as a definition in ~/.bash_profile. That means you get it when you personally login interactively, but not otherwise (like running a script). Cheers, David.
