diff options
| author | Sébastien Dailly <sebastien@chimrod.com> | 2021-01-10 22:00:38 +0100 |
|---|---|---|
| committer | Sébastien Dailly <sebastien@chimrod.com> | 2021-01-11 13:55:42 +0100 |
| commit | 85b40e5712fcbe76c697d1a22fb126db8079098c (patch) | |
| tree | 0aa2cd287f76c66b50b17c1e08fd30f59ba54a59 | |
| parent | 5ee27e786a3f1ed3eecc1e5c36f6e1e551388451 (diff) | |
Keep point selection after moving a point
| -rwxr-xr-x | script.it/state.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/script.it/state.ml b/script.it/state.ml index 107a72b..c147c2c 100755 --- a/script.it/state.ml +++ b/script.it/state.ml @@ -307,8 +307,7 @@ let do_action (fun p -> post worker (`Complete p)) (Path.Fixed.replace_point path point') ); - - { state with mode = Selection (Path id) } + { state with mode = Selection (Point (id, point')) } | `Delete, _ -> delete state worker |