mirror of
https://github.com/RIOT-OS/RIOT.git
synced 2024-12-29 04:50:03 +01:00
a9767889fc
Otherwise, when an error occurs (e.g. credentials wrong on git push) the worktree and the release branch still exists, which might be hard to remove for a newcomer not knowing about `git worktree`. |
||
---|---|---|
.. | ||
pythonlibs | ||
testbed-support | ||
tests/if_lib | ||
tools | ||
ar-wrapper | ||
empty.a | ||
gdbinit-docker | ||
Makefile |