Skip to content

opam source --dev PKG sets color.ui to false #6451

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
dbuenzli opened this issue Apr 1, 2025 · 3 comments
Open

opam source --dev PKG sets color.ui to false #6451

dbuenzli opened this issue Apr 1, 2025 · 3 comments

Comments

@dbuenzli
Copy link
Contributor

dbuenzli commented Apr 1, 2025

which I personally find undesirable, just let the user config take over.

> opam --version
2.3.0
> opam source --dev cmdliner
> git config --local color.ui
false
@dbuenzli dbuenzli changed the title opam source --dev repo sets color.ui to false opam source --dev repo sets color.ui to false Apr 1, 2025
@dbuenzli dbuenzli changed the title opam source --dev repo sets color.ui to false opam source --dev PKG sets color.ui to false Apr 1, 2025
@arozovyk
Copy link

arozovyk commented Apr 7, 2025

Related to #4883 and #4884

@dbuenzli
Copy link
Contributor Author

dbuenzli commented Apr 7, 2025

Note, regarding relationship to #4883. There is likely a distinction to be made between the git clones that opam does for itself and those that it does for me via opam source.

@kit-ty-kate
Copy link
Member

opam uses the same code to fetch git repository when using opam source or the other commands.
A distinction between the two was already made in #5888 so doing the same kind of change for avoiding all the git config settings when using opam source should be fairly easy to do.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

3 participants