what is --scratchdir= for?

[Duncan Coutts]

It's not clear to me what the configure --scratchdir= option is for. It
seems to be only used by hugs for building and installing and it
defaults to dist/scratch.

We don't allow any of the other locations under dist/scratch to be
overridden, probably because there's not much point in that. Why do we
need it for hugs?

If we're going to have an option like this it should probably set the
location of the whole dist/ directory hierarchy. Though that has its own
problems since we'd need to have --scratchdir= as a global option to
each command since we put the saved config info into $dist/ .

In the mean time, if we're keeping dist/ fixed then we can always just
rm -rf dist when doing a clean, fixing bug #92. If we allow the user to
override $dist then we'd have to be a bit more removing it since the
user could set it to some shared temp dir.

Duncan