From 5545969f485ef2fb944db8e7b0237acbabeb8d4c Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 7 Sep 2010 08:28:07 -0400 Subject: Server-side 'onError' --- src/expl.sml | 1 + 1 file changed, 1 insertion(+) (limited to 'src/expl.sml') diff --git a/src/expl.sml b/src/expl.sml index 1212383f..119c1d92 100644 --- a/src/expl.sml +++ b/src/expl.sml @@ -149,6 +149,7 @@ datatype decl' = | DStyle of int * string * int | DTask of exp * exp | DPolicy of exp + | DOnError of int * string list * string and str' = StrConst of decl list -- cgit v1.2.3