leanprover / LeanInk

LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.
Apache License 2.0
60 stars 16 forks source link

Removes duplicate bubbles after comment #44

Closed vanessa-rodrigues closed 1 year ago

vanessa-rodrigues commented 1 year ago

Description

There were identical bubbles after comments as shown in the following images:

MicrosoftTeams-image (1)

MicrosoftTeams-image (2)

This PR fixes this issue. Follows the example above after changes:

image

image

Additional Notes

Issue: https://github.com/orgs/leanprover-community/projects/3/views/1?pane=issue&itemId=16742242