Torbjorn Granlund tg at
Fri Dec 28 14:27:45 CET 2012

nisse at (Niels Möller) writes:

  It would make it a bit easier for other developers to
  1. Locate the files.
  2. Update the files.
  And I usually think version control is a good thing, also for web stuff.
  The files don't have to live in the main gmp repo, it could be a
  neighboring repo if that makes more sense.
There is now a local repo "www" parallel to the other gmp repos.
This repo is not visible through :8000, for performance reasons.

After having pushed a change, please execute the script www-update,
which lives in the same place.

One cannot delete things from the actual web server at the moment, since
some of the files in the target directory are auitomatically generated.
If I add --delete to rsync, then such files would disappear.  (This can
be fixed with --exclude, but let's please test this first.)

A first test would be if somebody added the suggested incompatibilities.


More information about the gmp-devel mailing list