-
New external top-level names were being created but the name cache wasn't being populated, leading to #7878. Signed-off-by: Jose Pedro Magalhaes <jpm@cs.ox.ac.uk>
ad1bc9dc
New external top-level names were being created but the name cache
wasn't being populated, leading to #7878.
Signed-off-by: Jose Pedro Magalhaes <jpm@cs.ox.ac.uk>