TU-Wien-dataLAB / Grader-Service

Grader Service offers lecturers and students a well integrated teaching environment for data science, machine learning and programming classes.
https://grader-service.readthedocs.io/en/latest/
BSD 3-Clause "New" or "Revised" License
27 stars 2 forks source link

Clean up local assignment git repo when push fails #171

Closed meffmadd closed 5 months ago

meffmadd commented 6 months ago

Describe the bug When a user's local git repo becomes too large, git cannot push the changes, and the push fails. Afterward, we do not remove the commit that was created for the push, which means the oversized commit is still in the git history and will prevent any future push calls.

Expected behavior The git repo should be cleaned after an error. For a failed push we should revert the commit and bring the repo to the same state as it was before the error.

Potential solution: git reset HEAD~1 and git gc