aboutsummaryrefslogtreecommitdiff
path: root/script.it/selection.mli
diff options
context:
space:
mode:
authorSébastien Dailly <sebastien@chimrod.com>2021-01-07 21:54:46 +0100
committerSébastien Dailly <sebastien@chimrod.com>2021-01-09 06:27:18 +0100
commit32618a5ce8e2b306af102e4c16711b090c36b840 (patch)
tree1c22b5bcf9f29e9ff0118cfa9aedd6fb05c9ab0f /script.it/selection.mli
parent6e5c6bf7beadc72e64e5d929e301b473b01c9303 (diff)
Allow point movement
Diffstat (limited to 'script.it/selection.mli')
-rwxr-xr-xscript.it/selection.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/script.it/selection.mli b/script.it/selection.mli
index 01f12dc..a405edc 100755
--- a/script.it/selection.mli
+++ b/script.it/selection.mli
@@ -2,6 +2,8 @@ type t =
| Path of int
| Point of (int * Path.Point.t)
+val threshold : float
+
(** Return the closest path from the list to a given point.
The path is returned with all thoses informations :