#
# In emergency situations, REAL_SHELL is used to perform shell commands
# from within the ghc driver script, by scribbling the command line to
#
# In emergency situations, REAL_SHELL is used to perform shell commands
# from within the ghc driver script, by scribbling the command line to