Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Corners in squares for pushout/pullback #11

Open
DavidJaz opened this issue Oct 4, 2017 · 2 comments
Open

Corners in squares for pushout/pullback #11

DavidJaz opened this issue Oct 4, 2017 · 2 comments
Labels
enhancement

Comments

@DavidJaz
Copy link

DavidJaz commented Oct 4, 2017

Fantastic editor! I am using it more and more. The main thing I find missing is the little corner cubes in squares saying that they are a pushout or a pullback. In tikzcd, these are accomplished with "phantom arrows", with only the endpoint showing (and set to \ulcorner, or \drcorner respectively).

Cheers,
@yishn
Copy link
Owner

yishn commented Oct 5, 2017

Thank you! Do you have any idea how to incorporate this into the UI?

@DavidJaz
Copy link
Author

DavidJaz commented Oct 5, 2017

Perhaps an extra button near the dashed/dotted/solid controls that allows for phantom?

@technicalguy technicalguy mentioned this issue Dec 23, 2017
Closed
yishn added a commit that referenced this issue Jan 25, 2020
@yishn
Support phantom arrows #11
e6decb8
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@yishn @DavidJaz