[m-dev.] for review: generate index files on web site

[Peter Ross]

On Mon, Jun 26, 2000 at 06:32:55PM +1000, David Glen JEFFERY wrote:
> We'll try again. Note that the solution implemented here will potentially
> cause problems if the different machines invoke generate_index_html at
> the same time. Is this worth worrying about?
> 
Maybe the best thing to do would be to output to index.html.$$ and then
move it to index.html at the end.

Check out ~mercury/logs/successful_tests.* to see the finishing times of
the various architectures.

Pete
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------