Re: HEADS UP: git repo WRONG push landed.

2023-07-18 Thread Chris Johns
d :-) > > Brett > > *From:* users on behalf of Karel Gardas > > *Sent:* Tuesday, July 18, 2023 7:58 AM > *To:* users@rtems.org > *Subject:* HEADS UP: git repo WRONG push landed. >   > [You don't often get em

Re: HEADS UP: git repo WRONG push landed.

2023-07-18 Thread Brett Sterling
The easiest way to do this is to revert and push. 'unpushing' is not recommended :-) Brett From: users on behalf of Karel Gardas Sent: Tuesday, July 18, 2023 7:58 AM To: users@rtems.org Subject: HEADS UP: git repo WRONG push landed. [You don&#

HEADS UP: git repo WRONG push landed.

2023-07-18 Thread Karel Gardas
Dear RTEMS users, if you are using RTEMS git repo, please do not pull now. Wrong patches landed in the main RTEMS git.rtems.org and they needs to be removed. Thanks for your patience! Karel Forwarded Message Subject: HEADS UP: git repo WRONG push landed. Date: Tue, 18