I don't want to delete mathlib/src

Stream: new members

[Martin Dvořák]

I am scared. This is what the GitHub's GUI offers me:

image.png

I don't want to delete mathlib/src. Is there any mechanism that will prevent me from doing so (in case I accidentally clicked the button)?

[Mario Carneiro]

Buttons with red text in github generally have an "are you sure" dialog

[Mario Carneiro]

But I don't know why you are seeing that. I see a green button labeled "code" at that location

[Martin Dvořák]

Mario Carneiro said:

Buttons with red text in github generally have an "are you sure" dialog

Thanks. That calmed me down. Still, I would like to know that it is really impossible for me (or anybody) to delete mathlib/src, no matter what buttons are pressed.

[Mario Carneiro]

You can create a PR that deletes mathlib/src, but don't expect it to be merged

[Alex J. Best]

Even if you did delete it on a branch it can easily be git reverted, and its unlikely you have push access to master so the worst you could do is mess up someones branch for a minute