Author	SHA1	Message	Date
David Himmelstrup	fb868cab9b	Run playground tests on PRs without deploying to GitHub Pages. (#148)	2020-09-03 15:32:41 +08:00
David Himmelstrup	cb5529aff8	Disable automatic snippet generation.	2020-09-02 19:42:52 +08:00
David Himmelstrup	917dc3693d	Improve the safety of the playground and limit the resources it may use. (#144) ... * Improve the safety of the playground and limit the resources it may use. * Don't send new code to server until 0.5s after the last keypress.	2020-08-28 14:49:55 +08:00
David Himmelstrup	b9d3966366	Fix coverage calculation.	2020-08-27 18:36:59 +08:00
David Himmelstrup	938b933b57	Compute doc coverage with stack rather than cabal.	2020-08-27 17:53:00 +08:00
David Himmelstrup	3956c046c3	CI: Change cache directories.	2020-08-22 13:00:25 +08:00
David Himmelstrup	8aa156796a	Improve caching for Github Pages.	2020-08-22 12:44:07 +08:00
David Himmelstrup	c5497b8c56	Clean up playground code.	2020-08-22 12:18:14 +08:00
David Himmelstrup	f1d945babb	Add missing snippet files.	2020-08-22 11:26:59 +08:00
David Himmelstrup	c1c4996e63	Simplify playground code and add snippets. (#136) ... * Add instructions for how to run the playground locally. * Make it easier to select backend in the elm code. * Use scrolling for long scripts. * Fix bug, send code to backend on connect, don't auto play on code changes. * Compile and cache snippets.	2020-08-22 10:35:25 +08:00
David Himmelstrup	ce6ea17c57	Try fixing paths again.	2020-08-21 09:45:06 +08:00
David Himmelstrup	fb176ead12	Fix gh-page paths.	2020-08-21 09:35:45 +08:00
David Himmelstrup	12025f2a2e	Don't minify playground.	2020-08-21 09:18:31 +08:00
David Himmelstrup	8c3e8acd3a	Playground (#134)	2020-08-21 08:52:19 +08:00
David Himmelstrup	b6975d705d	Don't build gh-pages for PRs.	2020-08-07 09:15:50 +08:00
David Himmelstrup	5e7efdb608	Maintain a github-page with HPC results and haddock coverage data. (#129)	2020-08-06 18:44:06 +08:00