[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Commit mistake?
|
From: |
Eli Zaretskii |
|
Subject: |
Re: Commit mistake? |
|
Date: |
Sun, 25 Nov 2018 19:06:39 +0200 |
> From: Stephen Berman <address@hidden>
> Cc: address@hidden
> Date: Sun, 25 Nov 2018 17:47:46 +0100
>
> > Just delete that file, it should not be in the repository. "git rm"
> > etc. (Let me know if you need more detailed instructions.)
>
> Do you mean a new commit using "git rm" on my local branch and then
> pushing it to master at Savannah
Yes.