Skip to content
Snippets Groups Projects
  1. Jul 13, 2018
  2. Jul 12, 2018
    • Giovanni's avatar
      Update pushdoc · 923de6b8
      Giovanni authored
      Small fix: do not push manual when building from a pull request
      923de6b8
  3. Jul 02, 2018
  4. Jun 12, 2018
  5. Jun 08, 2018
  6. Jun 06, 2018
  7. Jun 04, 2018
    • Giovanni Bussi's avatar
      small fix · 9e83e94e
      Giovanni Bussi authored
      just annoying when there are directories whose name contains a space
      within the src/ directory
      9e83e94e
  8. May 30, 2018
  9. May 28, 2018
  10. May 21, 2018
  11. May 16, 2018
  12. May 13, 2018
    • Giovanni Bussi's avatar
      Add check astyle · 6b598e34
      Giovanni Bussi authored
      Check first if astyle is present. In this way, when astyle is not compiled,
      we get a single error instead of one error per file.
      6b598e34
  13. May 12, 2018
  14. May 07, 2018
  15. May 02, 2018
  16. Apr 30, 2018
  17. Apr 05, 2018
  18. Apr 03, 2018
  19. Mar 22, 2018
Loading