Re: How often is the git repository is updated?

[Joel Brobecker <brobecker@adacore.com>]

> Here it is.  Joel, I guess you are the responsible for the web pages,
> right?  It this OK for pushing to htdocs repo?

In terms of approval, it's a bit of a grey area. I tend to consider
that this is documentation, and thus give Eli authority for approval,
but I often make "obvious" changes.

I think that this is sufficiently obvious that it's OK to check in.
We can always revise it later, if Eli has some comments. Go ahead
and check it in - this will automatically update sourceware.org.
I'll take care of the gnu.org side right after.

Thanks,
-- 
Joel