Re: [PATCH v1 1/1] srcu-cbmc: Use /usr/bin/awk instead of /bin/awk

[Josh Triplett <josh@joshtriplett.org>]

On Fri, Apr 21, 2017 at 09:52:10PM +0000, Kushwaha, Priyalee wrote:
> Tested 9 distros centos, Debian, Fedora, Gentoo, Opensuse, slackware, Ubuntu, poky showed awk at /usr/bin/awk. 
> 
> Here is another similar patch which has been approved https://patchwork.kernel.org/patch/9650581/
> 
> centos-7:
> lrwxrwxrwx 1 root root 4 Mar 15 19:58 /bin/awk -> gawk lrwxrwxrwx 1 root root 4 Mar 15 19:58 /usr/bin/awk -> gawk
> 
> Debian-8:
> ls: cannot access /bin/awk: No such file or directory lrwxrwxrwx 1 root root 21 Mar 20 23:26 /usr/bin/awk -> /etc/alternatives/awk
> 
> Fedora:
> lrwxrwxrwx. 1 root root 4 Sep 12  2016 /bin/awk -> gawk lrwxrwxrwx. 1 root root 4 Sep 12  2016 /usr/bin/awk -> gawk
> 
> Gentoo:
> lrwxrwxrwx 1 root root 15 Jan  1 13:57 /bin/awk -> ../usr/bin/gawk lrwxrwxrwx 1 root root  4 Jan  1 13:57 /usr/bin/awk -> gawk
> 
> Opensuse:
> lrwxrwxrwx 1 root root 21 Mar 20 11:19 /bin/awk -> /etc/alternatives/awk lrwxrwxrwx 1 root root 29 Mar 20 11:19 /usr/bin/awk -> /etc/alternatives/usr-bin-awk
> 
> Slackware:
> lrwxrwxrwx 1 root root  4 Mar 10 15:37 /bin/awk -> gawk lrwxrwxrwx 1 root root 13 Mar 10 15:37 /usr/bin/awk -> ../../bin/awk
> 
> Ubuntu:
> ls: cannot access '/bin/awk': No such file or directory lrwxrwxrwx 1 root root 21 Dec  6  2015 /usr/bin/awk -> /etc/alternatives/awk
> 
> Poky:
> ls: /bin/awk: No such file or directory
> lrwxrwxrwx    1 root     root            19 Apr 20 22:59 /usr/bin/awk

This seems fairly conclusive.  Based on this, switching over to
/usr/bin/awk seems fine.