diff --git a/scripts/config b/scripts/config index bb4d3deb6d1c..6b3272ef6ec7 100755 --- a/scripts/config +++ b/scripts/config @@ -1,6 +1,8 @@ #!/bin/bash # Manipulate options in a .config file from the command line +myname=${0##*/} + # If no prefix forced, use the default CONFIG_ CONFIG_="${CONFIG_-CONFIG_}" @@ -8,7 +10,7 @@ usage() { cat >&2 <