summaryrefslogtreecommitdiff
path: root/language
diff options
context:
space:
mode:
authorAlasdair2020-05-21 15:30:43 +0100
committerAlasdair2020-05-21 15:30:43 +0100
commit8320ddc4b19d622f8ab5ab8625dde45fccbf383b (patch)
tree4ebd634581c6ffe6c5b61ad9437692a1856a81c6 /language
parent3311b7d4c5aeebacdbcd14602d7a8a75a9c1b258 (diff)
parent92b0564856fb3e20a09bead04d5c1b21eed224e1 (diff)
Merge branch 'sail2' into mono-tweaks
Diffstat (limited to 'language')
-rw-r--r--language/jib.ott1
1 files changed, 1 insertions, 0 deletions
diff --git a/language/jib.ott b/language/jib.ott
index 63c86126..9c739ec4 100644
--- a/language/jib.ott
+++ b/language/jib.ott
@@ -57,6 +57,7 @@ grammar
name :: '' ::=
| id nat :: :: name
+ | global id nat :: :: global
| have_exception nat :: :: have_exception
| current_exception nat :: :: current_exception
| throw_location nat :: :: throw_location