diff options
author | Joris | 2020-01-30 11:35:31 +0000 |
---|---|---|
committer | Joris | 2020-01-30 11:35:31 +0000 |
commit | 960fa7cb7ae4c57d01306f78cd349f3a8337d0ab (patch) | |
tree | 5077cc720525fb025e4dba65a9a8b631862cbcc8 /public | |
parent | 14bdbc8c937f5d0b35c61350dba28cb41c3737cd (diff) | |
parent | 6a04e640955051616c3ad0874605830c448f2d75 (diff) |
Merge branch 'with-ghcjs' into 'master'
Use Haskell on the frontend
See merge request guyonvarch/shared-cost!2
Diffstat (limited to 'public')
-rw-r--r-- | public/css/reset.css | 12 | ||||
-rw-r--r-- | public/javascript/.gitkeep (renamed from public/javascripts/.gitkeep) | 0 | ||||
-rw-r--r-- | public/javascripts/main.js | 17 |
3 files changed, 0 insertions, 29 deletions
diff --git a/public/css/reset.css b/public/css/reset.css index 42f3b8c..2eecc94 100644 --- a/public/css/reset.css +++ b/public/css/reset.css @@ -56,17 +56,5 @@ button:hover { cursor: pointer; } button::-moz-focus-inner { border: 0; } :focus { outline: none; } -select:-moz-focusring { - color: transparent; - text-shadow: 0 0 0 #000; -} -select { - -webkit-appearance: none; - -moz-appearance: none; - text-indent: 1px; - text-overflow: ''; - cursor: pointer; -} - html { box-sizing: border-box; } *, *:before, *:after { box-sizing: inherit; } diff --git a/public/javascripts/.gitkeep b/public/javascript/.gitkeep index e69de29..e69de29 100644 --- a/public/javascripts/.gitkeep +++ b/public/javascript/.gitkeep diff --git a/public/javascripts/main.js b/public/javascripts/main.js deleted file mode 100644 index 3c3d797..0000000 --- a/public/javascripts/main.js +++ /dev/null @@ -1,17 +0,0 @@ -// Remove search query -window.history.pushState( - { - html: document.documentElement.innerHTML, - pageTitle: document.title - }, - '', - document.location.pathname + document.location.hash -); - -var app = Elm.Main.fullscreen({ - time: new Date().getTime(), - translations: JSON.parse(document.getElementById('translations').innerHTML), - conf: JSON.parse(document.getElementById('conf').innerHTML), - result: JSON.parse(document.getElementById('result').innerHTML), - windowSize: { width: window.innerWidth, height: window.innerHeight } -}); |