From 02b36b68748932b95188424e1ddbb44e174b824a Mon Sep 17 00:00:00 2001 From: Ting-Gian LUA Date: Thu, 7 Nov 2024 15:47:41 +0800 Subject: [PATCH] [ doc ] Update CHANGELOG for PR by @ChAoSUnItY --- CHANGELOG.md | 7 ++++++- lib/js/src/State/State__Command.bs.js | 4 ++-- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 20b20556..41115cd6 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,10 +9,15 @@ 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) + +### Changed +- Upgrade ReScript to v11 +- CI overhaul: allow testings be be conducted on all major platforms (Windows, macOS, Ubuntu) and on multiple versions of Agda ## v0.4.7 - 2023-12-16 -### Change +### Changed - Fetch the latest release of Agda Language Server from GitHub ### Fixed diff --git a/lib/js/src/State/State__Command.bs.js b/lib/js/src/State/State__Command.bs.js index a3098d1c..97051cf3 100644 --- a/lib/js/src/State/State__Command.bs.js +++ b/lib/js/src/State/State__Command.bs.js @@ -154,8 +154,8 @@ async function dispatchCommand(state, command) { var goal$1 = match$3[0]; if (match$3[1] === "") { return await State__View$AgdaModeVscode.Panel.prompt(state, header, { - body: "Please specify which variable you wish to split", - placeholder: "variable to case split:", + body: "Please specify which variable(s) you wish to split, multiple variables are delimited by whitespaces", + placeholder: "variable(s) to case split:", value: undefined }, (async function (expr) { if (expr === "") {