
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