diff options
| author | Joris | 2020-08-09 08:37:18 +0200 |
|---|---|---|
| committer | Joris | 2020-08-09 08:37:18 +0200 |
| commit | ad6abcd5fc5e4e66062c8a01b511a1bd4bda2e94 (patch) | |
| tree | 0dee6c63c45e34ce960ca6c445b4ee9dbdcb3087 /src/Lib/File.ml | |
| parent | 2cb752123d15916496e872c9fbd423c788c86c64 (diff) | |
| download | map-ad6abcd5fc5e4e66062c8a01b511a1bd4bda2e94.tar.gz map-ad6abcd5fc5e4e66062c8a01b511a1bd4bda2e94.tar.bz2 map-ad6abcd5fc5e4e66062c8a01b511a1bd4bda2e94.zip | |
Export as CSV
Diffstat (limited to 'src/Lib/File.ml')
| -rw-r--r-- | src/Lib/File.ml | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/Lib/File.ml b/src/Lib/File.ml new file mode 100644 index 0000000..0089001 --- /dev/null +++ b/src/Lib/File.ml @@ -0,0 +1,12 @@ +let download filename content = + let a = + H.a + [| HA.href ("data:text/plain;charset=utf-8," ^ URI.encode content) + ; HA.download filename + ; HA.style "display:none" + |] + [| |] + in + let () = Element.append_child Document.body a in + let () = Element.click a in + Element.remove_child Document.body a |