I don't use Jenkins, github, or github actions at my job, so I hadn't heard of a jenkinsfile before this discussion.
I don't see it mentioned in the documentation about how to set up ci/cd.
Other things I didn't know, but I don't know if they should be made known there perhaps are:
I didn't know that github had a jenkins action, which apparently it does, or something causes it to find a jenkinsfile and know that means to run some github actions.
I didn't know github could run an action from something not in the .github folder.
Probably people that use github or Jenkins or both probably know that stuff, and most plugin maintainers probably use their plugins, we just don't use the plugin ourselves in our development process.
Thanks,
Karl