IIUC, after each drdr build, it generates the report pages, and then
it dumps the built tree. If so, how about changing it: before the
tree is removed, it archives the built files (run `git ls-files -o')
and makes the archive available somewhere.
If this is done, then I can do the following:
1. Given that drdr is usually very busy, download new build archives
to someplace else (like pre.racket-lang.org)
2. Write some script that you'd run with `git pre-build', which would
check whether there's a build archive available for your current
HEAD. This means that after you've pulled new stuff into your
repo, you could just run this command and get a working tree very
quickly.
3. Even more: if there's no archive for your HEAD, it could check your
origin/master, and if that's part of your current HEAD history (as
happens after a `git pull --rebase'), it will still do that. This
means that you'd be left with a tree that has compiled results for
an older version, but with most uses of `pull --rebase', this means
that only files that you've worked on are outdated, so a followup
setup would usually be very quick.
4. Of course, that won't help with changes in src, and the script
could warn you about that. It also wouldn't help much if you have
edits in core files like in the `racket' collection.
--
((lambda (x) (x x)) (lambda (x) (x x))) Eli Barzilay:
http://barzilay.org/ Maze is Life!
_________________________________________________
For list-related administrative tasks:
http://lists.racket-lang.org/listinfo/dev
