Skip to content

dune_console: make refresh rate configurable and default INSIDE_EMACS to 15#8812

Merged
rgrinberg merged 1 commit intoocaml:mainfrom Alizter:ps/branch/dune_console__make_framerate_configurable_and_default_inside_emacs_to_15Oct 11, 2023
+51-11

Commits

Commits on Oct 11, 2023