()
| 132 | // Also works on Firefox and Edge. |
| 133 | |
| 134 | function updateState() { |
| 135 | history.replaceState( |
| 136 | { |
| 137 | left_top: split_left.scrollTop, |
| 138 | right_top: split_right.scrollTop |
| 139 | }, |
| 140 | document.title |
| 141 | ); |
| 142 | } |
| 143 | |
| 144 | function loadState(ev) { |
| 145 | if (ev) { |