srcu-cbmc: Use /usr/bin/awk instead of /bin/awk

Most OS distribution have awk in /usr/bin not in /bin
Without this patch, kernel-devsrc fails to build as
runtime dependency for srcu-cbmc script /bin/awk is
not found.

Signed-off-by: Kushwaha, Priyalee <priyalee.kushwaha@intel.com>
Acked-by: Lance Roy <ldr709@gmail.com>
Reviewed-by: Josh Triplett <josh@joshtriplett.org>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
This commit is contained in:
Priyalee Kushwaha 2017-04-22 10:17:11 -07:00 committed by Paul E. McKenney
parent 492b95e597
commit b562b85c3a
1 changed files with 1 additions and 1 deletions

View File

@ -1,4 +1,4 @@
#!/bin/awk -f #!/usr/bin/awk -f
# Modify SRCU for formal verification. The first argument should be srcu.h and # Modify SRCU for formal verification. The first argument should be srcu.h and
# the second should be srcu.c. Outputs modified srcu.h and srcu.c into the # the second should be srcu.c. Outputs modified srcu.h and srcu.c into the