This is an automated email from the git hooks/post-receive script. It was
generated because a ref change was pushed to the repository containing
the project "DejaGNU".
The branch, master has been updated
via 83c212039ac2f58d85447755187dc2dec3832370 (commit)
from a36720ae1442f4f59d4c2762246b5f820db7c001 (commit)
Those revisions listed above that are new to this repository have
not appeared on any other notification email; so we list those
revisions in full, below.
- Log -----------------------------------------------------------------
commit 83c212039ac2f58d85447755187dc2dec3832370
Author: Ben Elliston <[email protected]>
Date: Wed Dec 5 22:59:55 2018 +1100
* doc/dejagnu.texi (execute_anywhere Procedure): Remove obsolete
node.
-----------------------------------------------------------------------
Summary of changes:
ChangeLog | 5 +++++
doc/dejagnu.texi | 26 +-------------------------
2 files changed, 6 insertions(+), 25 deletions(-)
hooks/post-receive
--
DejaGNU
_______________________________________________
Dejagnu-commit mailing list
[email protected]
https://lists.gnu.org/mailman/listinfo/dejagnu-commit
