[config] Allow user to specify custom CONFIG_SHELL

In case the shell the user wants to use as CONFIG_SHELL is located in a
weird place (eg. /opt/bash/bin/bash), or is weirdly named (eg. bash-4),
let the user enter the patch to the shell.

 # Compute Alpha-specific values

 CT_DoArchTupleValues () {

     # The architecture part of the tuple:

     CT_TARGET_ARCH="${CT_ARCH}${CT_ARCH_ALPHA_VARIANT}"

     # The kernel ARCH:

     CT_KERNEL_ARCH=${CT_ARCH}

 }