steps:
- script: |
    set -e
    echo "Building documentation"
    make -C doc/ html
  displayName: Build documentation