Add basic gitpod config

Trying out gitpod.io to see if we can use it as a simple way to get people
a working dev environment to work on the documentation.
pull/908/head
Tim Head 2020-06-08 10:05:36 +02:00
rodzic bbc3ee02c0
commit bf3f46776a
1 zmienionych plików z 9 dodań i 0 usunięć

9
.gitpod.yml 100644
Wyświetl plik

@ -0,0 +1,9 @@
tasks:
- init: |
pip3 install -r docs/doc-requirements.txt
pip3 install -e.
command: |
cd docs && make html && cd build/html && python3 -m http.server 8080
name: Sphinx preview
ports:
- port: 8080