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

Jump to bottom

Common tests: Missing standard-library #3159

Closed
asr opened this issue Jul 18, 2018 · 0 comments
Closed

Common tests: Missing standard-library #3159

asr opened this issue Jul 18, 2018 · 0 comments
Assignees
@asr
Labels
infra: test suite Issues relating to the test suite (not in changelog) type: bug Issues and pull requests about actual bugs ux: library management Issues relating to the library management system
Milestone
2.5.4.1

Comments

@asr
Copy link
Member

asr commented Jul 18, 2018

After removing the .agda directory from my home directory, I'm getting the following error on the release-2.5.4 branch (but it works on master):

$ cd test/Common/
$ make
Bool.agda
Library 'standard-library' not found.
Add the path to its .agda-lib file to
  '$HOME/.agda/libraries'
to install.

¿Can someone reproduce this problem?
@asr asr added infra: test suite Issues relating to the test suite (not in changelog) type: discussion Discussions about Agda's design and implementation labels Jul 18, 2018
@asr asr added this to the 2.5.4.1 milestone Jul 18, 2018
@asr asr self-assigned this Jul 18, 2018
@asr asr closed this as completed in 0aadc72 Jul 18, 2018
@asr asr added type: bug Issues and pull requests about actual bugs ux: library management Issues relating to the library management system and removed type: discussion Discussions about Agda's design and implementation labels Jul 18, 2018
asr added a commit that referenced this issue Jul 18, 2018
@asr
[ fixed #3159 ] By replacing --no-default-libraries by `--no-librar…
cc50a47 
…ies`.

(cherry picked from commit 0aadc72)
asr added a commit that referenced this issue Jul 18, 2018
@asr
[ #3159 ] Added missing replace.
8f0c5d7 
Replaced `--no-default-libraries` by `--no-libraries`.
asr added a commit that referenced this issue Jul 18, 2018
@asr
[ #3159 ] Added missing replace.
6e23058 
Replaced `--no-default-libraries` by `--no-libraries`.

(cherry picked from commit 8f0c5d7)
asr added a commit that referenced this issue Jul 18, 2018
@asr
[ #3159 ] Added missings --no-default-libraries option.
61ab774
asr added a commit that referenced this issue Jul 18, 2018
@asr
[ #3159 ] Added missings --no-default-libraries option.
60ad93a 
(cherry picked from commit 61ab774)
asr added a commit that referenced this issue Jul 18, 2018
@asr
[ #3159 ] Added missing replace.
1aa797d 
Replaced `--no-default-libraries` by `--no-libraries`.

(cherry picked from commit 8f0c5d7)
asr added a commit that referenced this issue Jul 18, 2018
@asr
[ #3159 ] Added missings --no-default-libraries option.
c33d4a7 
(cherry picked from commit 61ab774)
asr added a commit that referenced this issue Jul 18, 2018
@asr
[ #3159 ] Added more missing --no-default-libraries options.
20a73f2
asr added a commit that referenced this issue Jul 18, 2018
@asr
[ #3159 ] Added more missing --no-default-libraries options.
267fb6d 
(cherry picked from commit 20a73f2)
asr added a commit that referenced this issue Jul 18, 2018
@asr
[ #3159 ] Added more missing --no-default-libraries options.
bfd18ad 
(cherry picked from commit 20a73f2)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@asr asr

Labels
infra: test suite Issues relating to the test suite (not in changelog) type: bug Issues and pull requests about actual bugs ux: library management Issues relating to the library management system
Projects
None yet
Milestone
2.5.4.1
Development

No branches or pull requests
1 participant
@asr