You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
With git's color.ui set to always, I get the following errors:
[ERROR] Could not update repository "bb-overlay-fork": "/usr/local/bin/patch -p1 -i /Users/pgiarrusso/.opam/log/processed-patch-58446-70a526" exited with code 2 "/usr/local/bin/patch: **** Only garbage was found in the patch input."
[bb-overlay] synchronised from git+https://github.com/Blaisorblade/opam-overlay.git
[ERROR] Could not update repository "bb-overlay": "/usr/local/bin/patch -p1 -i /Users/pgiarrusso/.opam/log/processed-patch-58446-e80101" exited with code 2 "/usr/local/bin/patch: **** Only garbage was found in the patch input."
[iris-dev] synchronised from git+https://gitlab.mpi-sws.org/iris/opam.git
[ERROR] Could not update repository "iris-dev": "/usr/local/bin/patch -p1 -i /Users/pgiarrusso/.opam/log/processed-patch-58446-8b8e2c" exited with code 2 "/usr/local/bin/patch: **** Only garbage was found in the patch input."
Maybe opam needs to override color.ui git settings, like it does (IIRC) for a few others (e.g. #3788)?
Tested on opam 2.0.8.
The text was updated successfully, but these errors were encountered:
With git's
color.ui
set toalways
, I get the following errors:Maybe
opam
needs to overridecolor.ui
git settings, like it does (IIRC) for a few others (e.g. #3788)?Tested on opam 2.0.8.
The text was updated successfully, but these errors were encountered: