| summaryrefslogtreecommitdiff |
diff options
| author | Nathanael Sensfelder <SpamShield0@MultiAgentSystems.org> | 2017-07-19 13:27:22 +0200 |
|---|---|---|
| committer | Nathanael Sensfelder <SpamShield0@MultiAgentSystems.org> | 2017-07-19 13:27:22 +0200 |
| commit | f14256ddd4129eb0e4ed331f2fa3d84b3618f0a6 (patch) | |
| tree | d4b9e81d4f1e39a539229d90e0626a53e71bff8f /instr-scripts/id_manager.py | |
| parent | 8f12413895954e5feed9ea915825d462f0457fe4 (diff) | |
Woops, the previous commit wasn't enough.
Diffstat (limited to 'instr-scripts/id_manager.py')
| -rw-r--r-- | instr-scripts/id_manager.py | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/instr-scripts/id_manager.py b/instr-scripts/id_manager.py index a406cd6..27c1474 100644 --- a/instr-scripts/id_manager.py +++ b/instr-scripts/id_manager.py @@ -11,6 +11,12 @@ class Id_Manager: result = str(self.next_id) self.next_id += 1 + self.output.write( + "(map_xml_id PURE " + + result + + ")\n" + ) + return result def generate_new_id (self, xml_id): |