#!/bin/bash # This script generate the settings.ini file used for GGA or GRM support NORMAL_FONT="\e[0m" RED_FONT="\e[31;1m" GREEN_FONT="\e[32;1m" YELLOW_FONT="\e[33;1m" GGA_GRM_ENABLE="$1" PATH_TO_SETTINGS_INI="$2" # No path specified, use default ../.. if [[ -z $PATH_TO_SETTINGS_INI ]]; then PATH_TO_SETTINGS_INI="../.."; echo -e "$RED_FONT File \"settings.ini\" will be stored into \"$PATH_TO_SETTINGS_INI/settings.ini\" (default)$NORMAL_FONT" >&2 fi # Only create settings.ini for 'gga' and 'gpu' options cat > $PATH_TO_SETTINGS_INI/settings.ini <> $PATH_TO_SETTINGS_INI/settings.ini <