Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Reduce log verbosity by printing less output for git commands #280

Open
Zimmi48 opened this issue Apr 26, 2023 · 2 comments
Open

Reduce log verbosity by printing less output for git commands #280

Zimmi48 opened this issue Apr 26, 2023 · 2 comments
Labels
enhancement New feature or request

Comments

@Zimmi48
Copy link
Member

Zimmi48 commented Apr 26, 2023

Currently, the output of git fetch or git merge can be arbitrarily long...
But we are limited in the size of logs that we can save for free with Papertrails.
@ticket-tagger ticket-tagger bot added the enhancement New feature or request label Apr 26, 2023
@Zimmi48
Copy link
Member Author

Zimmi48 commented Apr 27, 2023

Actually, what is even more problematic with respect to the log verbosity is to print the coq minimized files in the log (which can also be arbitrarily long, but are very often much longer than the git command outputs).

@Zimmi48
Copy link
Member Author

Zimmi48 commented Apr 27, 2023

I've done something for that in #276.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement New feature or request
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@Zimmi48