diff --git a/scripts/config b/scripts/config new file mode 100755 index 0000000000000000000000000000000000000000..68b9761cdc38aac39700fbd99b4c563d6c1ca3d6 --- /dev/null +++ b/scripts/config @@ -0,0 +1,150 @@ +#!/bin/bash +# Manipulate options in a .config file from the command line + +usage() { + cat >&2 <