[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] How do you delete a module?
Thanks. I got it working.
It's ironic that a software system build around correctness has such as wonky and persnickety IDE ;)
On 06.10.2018 15:21, Veronica Straszheim wrote:
> It seems if I create a specification, I automatically creates a module
> named "Untitled". I see no way to delete it. If I delete the file from
> my drive, it gets confused and spits errors at me.
> This is really weird and confusing. How does one use this software?
module deletion is unfortunately currently not possible. The
corresponding github issue  describes a workaround.
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.