Remove useless scripts from local/bin

[koffie]

sage-grep is not needed since we now have search_src same goes for sage-grep-doc
and sage-verify-pyc is not needed either and sage-sage.py is also useless right now, see: #21 comment:19

---

Apply

1. attachment: 12190-remove-old-scripts.patch.patch

to the sage-scripts repository.

CC: @saraedum

Component: misc

Keywords: sd35

Author: Maarten Derickx

Reviewer: Julian Rueth, Jeroen Demeyer

Merged: sage-4.8.alpha6

Issue created by migration from https://trac.sagemath.org/ticket/12190

[koffie]

Attachment: 12190-remove-old-scripts.patch.gz

[saraedum]

Reviewer: Julian Rueth

[saraedum]

Author: Maarten Derickx

[koffie]

Changed keywords from none to sd35

[jdemeyer]

comment:8

You should also remove the calls to these scripts from sage-sage.

[koffie]

Attachment: 12190-remove-old-scripts.patch.patch.gz

[jdemeyer]

Changed reviewer from Julian Rueth to Julian Rueth, Jeroen Demeyer

[jdemeyer]

comment:10

Looks good, thanks!

[jdemeyer]

Merged: sage-4.8.alpha6