For sure your opinion is valid and thank you for keeping the conversation going.openBrain wrote: ↑Mon Jul 22, 2019 5:04 pm What about having a server (maybe the one hosting the website ???) subscribing to GitHub hooks (PushEvent and PullRequestEvent are the 2 I see ATM) through the REST API to update commit ID & hash on somewhere else that would be merged at compile time ?
PS : guys, please tell me if I'm making more noise than helping...
Yes, there is a server that we can use, AFAIK. If we can work on a proposal and get consensus, we may be able to implement this.