aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-09-26 16:32:44 +0200
committerEmilio Jesus Gallego Arias2018-09-26 16:32:44 +0200
commitf49928874b51458fb67e89618bb350ae2f3529e4 (patch)
treec6abdf06041752d6239700c57840cc0d3d2a0f4d
parentef231c674c11f2f7f6d87bc45f6b909aca26f0c2 (diff)
parent4ea1dfb16a26959843b2db6fc398556c17abd682 (diff)
Merge PR #8561: Fix votour compilation after #8102.
-rw-r--r--checker/votour.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/checker/votour.ml b/checker/votour.ml
index bc820e23dd..1ea0de456e 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -152,6 +152,7 @@ let rec get_name ?(extra=false) = function
|String -> "string"
|Annot (s,v) -> s^"/"^get_name ~extra v
|Dyn -> "<dynamic>"
+ | Proxy v -> get_name ~extra !v
(** For tuples, its quite handy to display the inner 1st string (if any).
Cf. [structure_body] for instance *)
@@ -255,6 +256,7 @@ let rec get_children v o pos = match v with
| _ -> raise Exit
end
|Fail s -> raise Forbidden
+ | Proxy v -> get_children !v o pos
let get_children v o pos =
try get_children v o pos