fixup for d28e9ea: add support for clipboard.readText()

diff --git a/icedeb.js b/icedeb.js
index 902ba3bbb1826aac46eff8b9be676b3aa8e12c60..41117778fa9a08fc08acb30ff44b05acb69b465b 100644 (file)
--- a/icedeb.js
+++ b/icedeb.js
@@ -205,6 +205,7 @@ function check_likely_inputs(q) {
 }
 
 function react_to_clipboard_text(text) {
 }
 
 function react_to_clipboard_text(text) {

+  let clip_input = document.getElementById("clipboard");

   clip_input.value = text;
   clip_input.focus();
   clip_input.setSelectionRange(0, clip_input.value.length);
   clip_input.value = text;
   clip_input.focus();
   clip_input.setSelectionRange(0, clip_input.value.length);