Insert a line that was accidentally deleted

CakeML · Aug 18, 2022 · 0da134b · 0da134b
1 parent da3d6b8
commit 0da134b
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/basis/types.txt b/basis/types.txt
@@ -378,3 +378,4 @@ print: string -> unit
 print_app_list: string app_list -> unit
 print_int: int -> unit
 print_pp: PrettyPrinter.pp_data -> unit
+