It would be better if make, make doc and make demo could be executed on the server at every push, instead of relying on the person committing the code to remember to do this...
I imagine this would also avoid having the "doc" folder and the generated bc.js files as part of the git repository.
samvang
commented
1 week ago
It would be better if
make,make docandmake democould be executed on the server at every push, instead of relying on the person committing the code to remember to do this... I imagine this would also avoid having the "doc" folder and the generated bc.js files as part of the git repository.