Call linting jobs "lint" (instead of "ruff")

Developers are humans, too. They deserve being served by the principle of least surprise.

IOW, we want linting jobs to be called "lint", not "ruff". Linting and formatting are common CI tasks across modern (Web) technologies. Let's call them what they are called also elsewhere. 😻