Re: How often is the git repository is updated?

Re: How often is the git repository is updated?

[Sergio Durigan Junior]

On Tuesday, August 14 2012, I wrote:

> On Tuesday, August 14 2012, Jan Kratochvil wrote:
>
>> On Tue, 14 Aug 2012 13:14:07 +0200, Gyula Gubacsi wrote:
>>> Read-only git section it is stated that the git mirror is updated
>>> regularly. How often I wonder? Wouldn't be a bit more precise to state
>>> the actual time interval?
>>
>> 30 minutes, see:
>> 	http://sourceware.org/ml/gdb/2009-10/msg00363.html
>
> I always thought it was 15 minutes.  Anyway, I agree with Gyula, it
> would be good to provide this info on the page.  I will send a patch to gdb-patches.

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

Thanks,

-- 
Sergio

Index: current/index.html
===================================================================
RCS file: /cvs/gdb/htdocs/current/index.html,v
retrieving revision 1.43
diff -u -p -r1.43 index.html
--- current/index.html	7 May 2009 14:45:33 -0000	1.43
+++ current/index.html	14 Aug 2012 18:25:07 -0000
@@ -155,8 +155,9 @@ cvs -d :ext:YOURACCOUNT@sourceware.org:/
 
 A read-only git mirror of GDB's repository is also available.
 This repository is not a real-time mirror, but is automatically
-resynchronized at regular intervals. To get a copy of that
-repository, use the following command:
+resynchronized at regular intervals, currently every 30 minutes.
+
+To get a copy of that repository, use the following command:
 
 <pre>
 git clone git://sourceware.org/git/gdb.git

Re: How often is the git repository is updated?

[Joel Brobecker]

> 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

Re: How often is the git repository is updated?

[Sergio Durigan Junior]

On Tuesday, August 14 2012, Joel Brobecker wrote:

>> 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, checked in.  I could not find a ChangeLog file to edit, so I
just committed the html.

-- 
Sergio

Re: How often is the git repository is updated?

[Joel Brobecker]

> Thanks, checked in.  I could not find a ChangeLog file to edit, so I
> just committed the html.

Yes, that's good enough. I propagated the change to gnu.org as well.

Thanks, Sergio.
-- 
Joel