checkpoint

Author: Aslan Askarov

body.tex

@@ -909,7 +909,7 @@ \subsubsection{\code{pinipushto}}
     \item [Arguments] A tuple: a value of type authority, and a level.
     \item [Returns] A string capability to be passed as the argument to \code{pinipop}
     \item [Failure behavior] Crashes if the current blocking level does not flow to the level argument.
-    \item [Example usage] \textcode{pinipushto (authority, {bob})}
+    \item [Example usage] \textcode{pinipushto (authority, \{bob\})}
 \end{description}