what is --scratchdir= for?

[ross at soi.city.ac.uk]

Quoting Duncan Coutts <duncan.coutts at worc.ox.ac.uk>:
> 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.

Yes, --scratchdir is a hack for the Hugs build that allows it to build
libraries that can be run inplace prior to installation.  An option to
move the whole of dist wouldn't be a replacement.

I also think an option to move dist would introduce too many complications.

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.