added checkbox graphics element

2023-07-01 19:40:33 -04:00
parent b6835fc7d1
commit 7b9824b6f9
2 changed files with 85 additions and 0 deletions
--- a/graphics/element.lua
+++ b/graphics/element.lua
@@ -20,6 +20,7 @@ local element = {}

 ---@alias graphics_args graphics_args_generic
 ---|waiting_args
+---|checkbox_args
 ---|hazard_button_args
 ---|multi_button_args
 ---|push_button_args