- comment to GitLab merge-request does not anymore # as number (misinterpreted as issue number)
- added local build script w/ generation of HTML result file
Improvements on bash scripts:
- use of proper option parsing
Signed-off-by: Raphael Defosseux <raphael.defosseux@eurecom.fr>