$include_dir="/home/hyper-archives/boost/include"; include("$include_dir/msg-header.inc") ?>
Subject: Re: [boost] git reset and force push
From: Raffi Enficiaud (raffi.enficiaud_at_[hidden])
Date: 2015-10-07 16:46:42
Le 07/10/15 22:44, Raffi Enficiaud a écrit :
> That is also a surprise: why so? the runner API is running the run.py
> script that is cloning/pulling things: it does not check out any branch,
> so it does not care if develop changed by history rewrite.
I am referring to a submodule there.