Skip to content

Better listing of separated components#13

Merged
dra27 merged 2 commits intotrunkfrom
abandoned
Apr 30, 2020
Merged

Better listing of separated components#13
dra27 merged 2 commits intotrunkfrom
abandoned

Conversation

@dra27
Copy link
Copy Markdown
Owner

@dra27 dra27 commented Apr 29, 2020

cc @gasche

Copy link
Copy Markdown

@gasche gasche left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Very nice, thanks!

Co-authored-by: Gabriel Scherer <gabriel.scherer@gmail.com>
@dra27 dra27 merged commit 67dc8fe into trunk Apr 30, 2020
@dra27 dra27 deleted the abandoned branch April 30, 2020 12:26
@dra27
Copy link
Copy Markdown
Owner Author

dra27 commented Apr 30, 2020

Excellent, ta - I shall push this to trunk shortly (and note that on caml-devel)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants