config: replace cli with direct common_ options

This commit is contained in:
Ciro Santilli
2018-08-09 07:12:20 +01:00
parent 1cb056a995
commit b1bd45684f
14 changed files with 10 additions and 45 deletions

View File

@@ -1,7 +1,5 @@
#!/usr/bin/env bash
set -eu
. "$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)/common"
set -- ${cli_rungdb_user:-} "$@"
usage="$0 <exec-relative-path> [<brk-symbol>]"
gem5_opt=
while getopts a:gh OPT; do