<!DOCTYPE html>
<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body>
<p>Hi,</p>
<p>I've got a push tree since several years, and it changed its
behavior a few weeks ago:</p>
<p>git reset --hard origin/master</p>
<p>now preserve my changes. Which option should I use to discard all
my changes?</p>
<p>Thanks</p>
<p>Laurent<br>
</p>
<div id="grammalecte_menu_main_button_shadow_host"
style="width: 0px; height: 0px;"></div>
</body>
</html>