From 80cd84ef1319e71b3b3dcc6ea83e078093ac8e8b Mon Sep 17 00:00:00 2001 From: Richard Brooksby Date: Tue, 31 Jan 2023 18:40:07 +0000 Subject: [PATCH] Fixing git command for pushing a fresh ci branch. --- mps/procedure/pull-request-merge.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mps/procedure/pull-request-merge.rst b/mps/procedure/pull-request-merge.rst index 0e24ea53628..5d83ad18b12 100644 --- a/mps/procedure/pull-request-merge.rst +++ b/mps/procedure/pull-request-merge.rst @@ -308,7 +308,7 @@ working repo before that point. on GitHub`_. This should trigger CI to build and testing on all target platforms. :: - git push github merge/2023-01-06/speed-hax + git push github HEAD:merge/2023-01-06/speed-hax You will need to wait for results from CI. Look for a build results in the `Travis CI build history for the repo`_ and in the