On Wed, Jul 13, 2022 at 03:06:48PM +, Klemens Nanni wrote:
> On Wed, Jul 13, 2022 at 01:38:59PM +, Klemens Nanni wrote:
> > On Wed, Jul 13, 2022 at 01:11:33PM +, Klemens Nanni wrote:
> > > On Mon, Jul 11, 2022 at 11:17:55AM +, Klemens Nanni wrote:
> > > > GH_* ports obviously set MA
On Wed, Jul 13, 2022 at 01:38:59PM +, Klemens Nanni wrote:
> On Wed, Jul 13, 2022 at 01:11:33PM +, Klemens Nanni wrote:
> > On Mon, Jul 11, 2022 at 11:17:55AM +, Klemens Nanni wrote:
> > > GH_* ports obviously set MASTER_SITES to MASTER_SITES_GITHUB which
> > > defaults github.com/${acc
On Wed, Jul 13, 2022 at 01:11:33PM +, Klemens Nanni wrote:
> On Mon, Jul 11, 2022 at 11:17:55AM +, Klemens Nanni wrote:
> > GH_* ports obviously set MASTER_SITES to MASTER_SITES_GITHUB which
> > defaults github.com/${account}/${project}/archive/${commit-or-tag}.
> >
> > If additional patch
On Mon, Jul 11, 2022 at 11:17:55AM +, Klemens Nanni wrote:
> GH_* ports obviously set MASTER_SITES to MASTER_SITES_GITHUB which
> defaults github.com/${account}/${project}/archive/${commit-or-tag}.
>
> If additional patches need to be fetched, e.g. pending PRs to fix the
> local port, addition
On Tue, Jul 12, 2022 at 11:08:30PM +, Klemens Nanni wrote:
> On 13/07/2022 02:52, Stuart Henderson wrote:
> > On 2022/07/12 08:41, Aaron Bieber wrote:
> > > On Mon, 11 Jul 2022 at 11:17:55 +, Klemens Nanni wrote:
> > > > GH_* ports obviously set MASTER_SITES to MASTER_SITES_GITHUB which
> >
On 13/07/2022 02:52, Stuart Henderson wrote:
On 2022/07/12 08:41, Aaron Bieber wrote:
On Mon, 11 Jul 2022 at 11:17:55 +, Klemens Nanni wrote:
GH_* ports obviously set MASTER_SITES to MASTER_SITES_GITHUB which
defaults github.com/${account}/${project}/archive/${commit-or-tag}.
If additional
On 2022/07/12 08:41, Aaron Bieber wrote:
> On Mon, 11 Jul 2022 at 11:17:55 +, Klemens Nanni wrote:
> > GH_* ports obviously set MASTER_SITES to MASTER_SITES_GITHUB which
> > defaults github.com/${account}/${project}/archive/${commit-or-tag}.
> >
> > If additional patches need to be fetched, e.
On Mon, 11 Jul 2022 at 11:17:55 +, Klemens Nanni wrote:
> GH_* ports obviously set MASTER_SITES to MASTER_SITES_GITHUB which
> defaults github.com/${account}/${project}/archive/${commit-or-tag}.
>
> If additional patches need to be fetched, e.g. pending PRs to fix the
> local port, additional
GH_* ports obviously set MASTER_SITES to MASTER_SITES_GITHUB which
defaults github.com/${account}/${project}/archive/${commit-or-tag}.
If additional patches need to be fetched, e.g. pending PRs to fix the
local port, additional MASTER_SITES0-9 must be defined which always
duplicate the GH_* values
