- 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>