-
Notifications
You must be signed in to change notification settings - Fork 17
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
c-c c-v verify should ask to save the current file #129
Comments
Does C-c ! C-c fstar work for this? |
Clement,
It just says "cannot use syntax checker fstar in this buffer".
Interesting you'd ask, Brian
…On Mon, Mar 20, 2023 at 4:02 PM Clément Pit-Claudel < ***@***.***> wrote:
Does C-c ! C-c fstar work for this?
—
Reply to this email directly, view it on GitHub
<#129 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/ACKMDK3PM3X63DPZAD3232TW5DOWRANCNFSM6AAAAAAV7UD2RY>
.
You are receiving this because you authored the thread.Message ID:
***@***.***>
|
Ah, right because it's using the server. That's a bit annoying. |
Clement,
Shall I fix it for you?
Thanks, Brian
…On Fri, Mar 24, 2023, 12:07 AM Clément Pit-Claudel ***@***.***> wrote:
Ah, right because it's using the server. That's a bit annoying.
Then I agree, it would be good to offer to save the buffer.
—
Reply to this email directly, view it on GitHub
<#129 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/ACKMDK3JYKAG2LZLXS2LWGDW5VB3BANCNFSM6AAAAAAV7UD2RY>
.
You are receiving this because you authored the thread.Message ID:
***@***.***>
|
Well, it wouldn't be for me (I don't use F* these days), but if you want to write the patch, that would be great! |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
When you want to verify on the command line, fstar-mode should check if the current buffer is saved
and do a save current file ask of the user.
The text was updated successfully, but these errors were encountered: