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

Remove useless scripts from local/bin #12189

Closed
koffie opened this issue Dec 19, 2011 · 2 comments
Closed

Remove useless scripts from local/bin #12189

koffie opened this issue Dec 19, 2011 · 2 comments
Labels
r: duplicate

Comments

@koffie
Copy link

koffie commented Dec 19, 2011

sage-grep is not needed since we now have search_src same goes for sage-grep-doc
and sage-verify-pyc is not needed eiter.

Component: PLEASE CHANGE

Issue created by migration from https://trac.sagemath.org/ticket/12189
@koffie koffie added this to the sage-4.8 milestone Dec 19, 2011
@koffie
Copy link
Author

koffie commented Dec 19, 2011

comment:1

Sorry for the duplicate (see #12189)

@koffie koffie removed this from the sage-4.8 milestone Dec 19, 2011
@koffie koffie closed this as completed Dec 19, 2011
@koffie
Copy link
Author

koffie commented Dec 19, 2011

comment:2

#12190

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
r: duplicate
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@koffie