annotate sat/VERSION @ 3167:d0fb79f97466

quick frontends (app): added an "ignore_missing" argument to RemoveListener: normally an error is logged when removeListener is call on a inexisting listener, but sometimes listeners are added only in specific scenarios, and it may be handy to try to delete them without having to explictly check that they have been used.
author Goffi <goffi@goffi.org>
date Wed, 12 Feb 2020 19:44:05 +0100
parents ff5bcb12ae60
children efe2445b053c
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
3027
ff5bcb12ae60 0.8 development starts
Goffi <goffi@goffi.org>
parents: 3025
diff changeset
1 0.8.0D