# as the driver script treats these guys specially and needs to carefully be told
# about the options for these. Hence, we hide the required command line options
# for these in the ghc/driver, as this is the only place they are needed.
#
# If you want to add to these default options, fill in the variables below:
# as the driver script treats these guys specially and needs to carefully be told
# about the options for these. Hence, we hide the required command line options
# for these in the ghc/driver, as this is the only place they are needed.
#
# If you want to add to these default options, fill in the variables below: