Skip to content

Commit 5d12253

Browse files
committed
Add missing '`' arguments surrounding level arguments
1 parent 1503432 commit 5d12253

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

body.tex

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -996,7 +996,7 @@ \subsubsection{\code{pinipushto}}
996996
\item [Arguments] A tuple: a value of type authority, and a level.
997997
\item [Returns] A string capability to be passed as the argument to \code{pinipop}
998998
\item [Failure behavior] Crashes if the current blocking level does not flow to the level argument.
999-
\item [Example usage] \textcode{pinipushto (authority, \{bob\})}
999+
\item [Example usage] \textcode{pinipushto (authority, `\{bob\}`)}
10001000
\end{description}
10011001

10021002

@@ -1025,7 +1025,7 @@ \subsubsection{\code{raiseTrust}}
10251025
\item [Returns] Unit.
10261026
\item [Failure behavior]. Fails if the argument type is invalid. Fails if the authority argument is not top.
10271027
Fails if the blocking level is not $\bot$.
1028-
\item [Example usage] $\code{raiseTrust("@alicescomputer", authority, \{alice\})}$
1028+
\item [Example usage] $\code{raiseTrust("@alicescomputer", authority, `\{alice\}`)}$
10291029
\end{description}
10301030
Note that the top-level authority is required because this is a privileged operation with system-wide consequences.
10311031

0 commit comments

Comments
 (0)