As documented in readme, this will break when converting to Unicode: ```tla ---- MODULE Test ---- op == /\ A (***) /\ \/ B (******) \/ C (***) => D ==== ``` The currently-ignored test `test_block_comments_prefixing_jlist_items` checks for this.