On 12/4/2018 10:34 AM, Rene Rivera via Boost wrote:
On Tue, Dec 4, 2018 at 9:28 AM Edward Diener via Boost < boost@lists.boost.org> wrote:
On 12/4/2018 8:03 AM, Rene Rivera via Boost wrote:
On Tue, Dec 4, 2018 at 4:03 AM Andrey Semashev via Boost < boost@lists.boost.org> wrote:
Yes, I'm in favor of adding some sort of a server-side git hook. For that all script files need to have an appropriate extension so that they can be whitelisted to have an executable permission. Though I'm not sure how server-side git hooks work with GitHub.
I don't think there's anything like git server-side hooks.
https://git-scm.com/docs/githooks and https://git-scm.com/book/en/v2/Customizing-Git-Git-Hooks suggest otherwise, although understanding how to write a hook from the sparse documentation seems difficult to me. Maybe someone who has written a git hook before understands how we can cycle through the files in a 'git push' and, if one of those files is a source file with its executable bit set, reject the push.
GitHub doesn't allow those server side hooks.
Are you saying that we have no access to the .git or .git/hooks subdirectory of a Github hosted repository ?