Trouble with git reset in my pushtree

[Ilmari Lauhakangas]

On 28.7.2024 11.25, Laurent Balland wrote:
> Hi,
> 
> I've got a push tree since several years, and it changed its behavior a 
> few weeks ago:
> 
> git reset --hard origin/master
> 
> now preserve my changes. Which option should I use to discard all my 
> changes?

In the .git/config file of LibreOffice source code, what is the value of 
url in the [remote "origin"] block?

Ilmari