** If you have a GerritForge Enterprise Support contract, file a bug through https://support.gerritforge.com instead **
** If you are interested in activating a new Support contract, use the https://gerritforge.com/contact form instead **
** This is for bugs in Gerrit sites hosted at *.gerrithub.io **

GerritHub/GitHub username: myitcv

GerritHub/GitHub projects names: https://review.gerrithub.io/admin/repos/cue-sh/tools,general

Full URL exhibiting the problem: n/a

Expected behavior:

We plan to migrate https://github.com/cue-sh/tools to a new location and rename to https://github.com/cue-lang/contrib-tools. Per the link above, https://github.com/cue-sh/tools is currently a mirror of https://review.gerrithub.io/admin/repos/cue-sh/tools,general. But before we do the move and rename, we would like to know what to do on the GerritHub side of things.

Unclear what the expected behaviour here should be; I couldn't find any docs that helped to answer the question.

Observed behavior: n/a

Timestamp when the error occurred (include timezone): n/a

Has this worked before? If yes, when? n/a

If applicable: screenshot of erroneous UI element: n/a

If applicable: JavaScript console log (chrome: F12 > Console): n/a

If applicable: Browser (name, version, operating system): n/a

If using git command-line: output of "which git && git --version": n/a

Any help much appreciated!

Issue 353167433

Links (9)

Issue metadata