diff options
| author | Neels Hofmeyr <neels@hofmeyr.de> | 2018-03-26 15:01:38 +0200 |
|---|---|---|
| committer | Neels Hofmeyr <neels@hofmeyr.de> | 2018-03-26 15:04:32 +0200 |
| commit | 71f781c303bb4216d3328181d7798a28a15813c9 (patch) | |
| tree | 337844d54cb809734e7ca18fa6c5cb9106bb49b1 /contrib/jenkins_common.sh | |
| parent | 338d17439973a7f2f54efc75bb8d40f6b9b8ff40 (diff) | |
contrib/fsm-to-dot: warn about identically named FSMs
FSMs with identical names confuse the script, so at least warn about them.
IMHO we should also have different names for each FSM, so not bothering to make
the script safe against identical naming.
Change-Id: I4fe7e85d2fdf23e2ba964f3b47be1954edc63cef
Diffstat (limited to 'contrib/jenkins_common.sh')
0 files changed, 0 insertions, 0 deletions