Re: [tlaplus] How do you delete a module?

[Veronica Straszheim <veronica...@xxxxxxxxx>]

Thanks. I got it working.

It's ironic that a software system build around correctness has such as wonky and persnickety IDE ;)

On Sat, Oct 6, 2018 at 6:57 PM Markus Kuppe <tlaplus-go...@xxxxxxxxxxx> wrote:

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?


Hi Veronica,

module deletion is unfortunately currently not possible. The
corresponding github issue [1] describes a workaround.

Thanks
Markus

[1] https://github.com/tlaplus/tlaplus/issues/195

--
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.