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

fix instructions for Installation of the Development Version #3105

Closed
wants to merge 1 commit into from
Closed

fix instructions for Installation of the Development Version #3105

wants to merge 1 commit into from

Conversation

halfaya
Copy link
Member

@halfaya halfaya commented Jun 4, 2018

No description provided.

@asr asr self-requested a review June 4, 2018 13:45
Copy link
Member

@asr asr left a comment

Choose a reason for hiding this comment

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

The current documentation is the "Agda User Manual, Release X.Y.Z", so instructions for installing the upstream version shouldn't be in the user manual, but elsewhere. I suggest to add these instructions in the Wiki.

@halfaya
Copy link
Member Author

halfaya commented Jun 4, 2018

These instructions were already in the user manual--I was merely correcting a mistake. I personally think they are fine in the manual--it's an easy location to find the instructions. I'd like to get rid of the various wiki pages many of which are outdated, and have a single unified source for information, which would be the user manual.

@asr
Copy link
Member

asr commented Jun 4, 2018

I was merely correcting a mistake.

You are right.

Please close this PR and create a new one using the stable-2.5 branch.

@halfaya
Copy link
Member Author

halfaya commented Jun 4, 2018

Yes, thanks, I am at AIM now and was told I need to do the PR against stable. Closing.

@halfaya halfaya closed this Jun 4, 2018
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