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