[ doc ] Update CHANGELOG for PR by @vic0103520

jiangsy · Nov 7, 2024 · c56ee86 · c56ee86
1 parent a61be3d
commit c56ee86
Show file tree

Hide file tree

Showing 12 changed files with 265 additions and 345 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -10,6 +10,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Fixed
 - #195: Remove all usage of deprecated api @bs.send.pipe by [@jiangsy](https://github.com/jiangsy)
 - #191: Add more detailed splitting command description by [@ChAoSUnItY](https://github.com/ChAoSUnItY)
+- #169: Custom Agda buffer font size in the extension's setting by [@vic0103520](https://github.com/vic0103520)
 
 ### Changed
 - Upgrade ReScript to v11

diff --git a/lib/js/src/Config.bs.js b/lib/js/src/Config.bs.js
diff --git a/lib/js/src/Main.bs.js b/lib/js/src/Main.bs.js
diff --git a/lib/js/src/State/State__View.bs.js b/lib/js/src/State/State__View.bs.js
diff --git a/lib/js/src/View/Panel/Panel.bs.js b/lib/js/src/View/Panel/Panel.bs.js