From bf3f46776ab6c725cf9158925f1ee2d1c96dadc0 Mon Sep 17 00:00:00 2001
From: Tim Head <betatim@gmail.com>
Date: Mon, 8 Jun 2020 10:05:36 +0200
Subject: [PATCH] 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.
---
 .gitpod.yml | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 .gitpod.yml

diff --git a/.gitpod.yml b/.gitpod.yml
new file mode 100644
index 00000000..c15d1534
--- /dev/null
+++ b/.gitpod.yml
@@ -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