diff options
Diffstat (limited to 'index.html')
| -rw-r--r-- | index.html | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/index.html b/index.html new file mode 100644 index 0000000..549b2cb --- /dev/null +++ b/index.html @@ -0,0 +1,18 @@ +<!DOCTYPE html> +<html> + <head> + <title>Coq commands counter</title> + </head> + <body> + <textarea id="input" cols="60" rows="20"></textarea><br/> + <textarea id="output" cols="60" rows="2"></textarea> + + <script type="text/javascript" src="//code.jquery.com/jquery-1.11.3.min.js"></script> + <script type="text/javascript" src="coqCounter.js"></script> + <script type="text/javascript"> + $(function(){ + $('#input').coqCounter('#output'); + }); + </script> + </body> +</html>
\ No newline at end of file |