TLA+ Toolbox nightly: Periodic workspace save java.lang.NumberFormatException

[Jaak Ristioja <jaak.r...@xxxxxxxx>]

Hi!

I'm periodically getting the following error from the nightly TLA+
toolbox build:

  !ENTRY org.eclipse.core.jobs 4 2 2015-12-02 16:29:34.751
  !MESSAGE An internal error occurred during: "Periodic workspace save.".
  !STACK 0
  java.lang.NumberFormatException: null
          at java.lang.Integer.parseInt(Integer.java:454)
          at java.lang.Integer.<init>(Integer.java:677)
          at
org.eclipse.core.internal.resources.SaveManager.validateMasterTableBeforeSave(SaveManager.java:1618)
          at
org.eclipse.core.internal.resources.SaveManager.saveMasterTable(SaveManager.java:1283)
          at
org.eclipse.core.internal.resources.SaveManager.saveMasterTable(SaveManager.java:1275)
          at
org.eclipse.core.internal.resources.SaveManager.save(SaveManager.java:1252)
          at
org.eclipse.core.internal.resources.SaveManager.save(SaveManager.java:1163)
          at
org.eclipse.core.internal.resources.DelayedSnapshotJob.run(DelayedSnapshotJob.java:52)
          at org.eclipse.core.internal.jobs.Worker.run(Worker.java:55)

The GUI error message dialog was not very informative:

  Problem Occurred

    'Periodic workspace save.' has encountered a problem.

    An internal error occurred during: "Periodic workspace save.".

                 [ OK ] [ << Details ]

    An internal error occurred during: "Periodic workspace save.".
      null


Best regards,
Jaak