Skip to content
Snippets Groups Projects
Commit 0e532ea5 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'robbert/as_ident_name_fix' into 'master' 

Fix bug in hint for `AsIdentName` when term is not a lambda.

See merge request iris/iris!936
parents ab3024b1 54aef63c
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment