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.

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

(doc) add Lean language #2464

Merged
merged 1 commit into from
Mar 21, 2020
Merged

(doc) add Lean language #2464

merged 1 commit into from
Mar 21, 2020

Conversation

bryangingechen
Copy link
Contributor

This is a followup to #1689. We've created a new repository at https://github.com/leanprover-community/highlightjs-lean and linked to it in SUPPORTED_LANGUAGES.md.

I'm not 100% sure we've made the new repo in the recommended way, so if a highlightjs maintainer would like to take a look and give some suggestions, I'd be very grateful!

cc: @PatrickMassot.

@joshgoebel
Copy link
Member

joshgoebel commented Mar 21, 2020

It'd be nice if you ran the build script and then committed the distributable to your repo. Unless you purposely aren't wanting that?

I see you have build instructions in the readme.

@joshgoebel joshgoebel merged commit 33a6718 into highlightjs:master Mar 21, 2020
@bryangingechen
Copy link
Contributor Author

Is it useful for people to see the minified version in the repo? I generally don't commit build outputs to version control, so I'm curious to know the reasons for doing so here.

@joshgoebel
Copy link
Member

joshgoebel commented Mar 21, 2020

I generally don't commit build outputs to version control, so I'm curious to know the reasons for doing so here.

Just so users desiring to use it on the web have a one click download or easy copy/paste, etc... not everyone has a build environment or the ability to set one up. Unless you're providing some other easy one-click download link?

@joshgoebel
Copy link
Member

Is it useful for people to see the minified version in the repo?

It's not JUST minified, it's compiled specifically for auto-loading CDN-style support.

@bryangingechen
Copy link
Contributor Author

Understood, thank you!

bryangingechen added a commit to leanprover-community/highlightjs-lean that referenced this pull request Mar 21, 2020
@bryangingechen bryangingechen deleted the lean branch March 21, 2020 19:13
@joshgoebel
Copy link
Member

Thanks for the contribution!

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.

None yet

2 participants