diff options
| author |  Jason Gross <jasongross9@gmail.com> | 2015-07-22 15:02:30 -0700 |
|---|---|---|
| committer |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-07-23 07:11:24 +0200 |
| commit | 4456b5edc3e2e62624e5251ff1e01dd81fabb29b (patch) | |
| tree | 4957752da1fd1f7a9e237ca662e014851e0e4d84 /tools/coqdep_common.ml | |
| parent | 92dfc77c7496297e094e2d39790a205d548b31da (diff) | |
Silence `which`
On Fedora, `which 2>&1 >/dev/null` doesn't silence stderr, while `which >/dev/null 2>&1` does.
Diffstat (limited to 'tools/coqdep_common.ml')
0 files changed, 0 insertions, 0 deletions