Ticket #12333: trac_12333_restore_grep_scripts.patch

File trac_12333_restore_grep_scripts.patch, 680 bytes (added by fwclarke, 16 months ago)

apply to scripts repository

  • new file sage-grep 

    # HG changeset patch
# User Francis Clarke <francis.w.clarke@gmail.com>
# Date 1327690023 0
# Node ID 2a162f8ecdfc7dd7aba176425663cf57c396171c
# Parent  4ee7dfb8cc30bb009f8fd2ec1c7a704bc76fe0f8
Trac 12333: Restore sage -grep (and -grepdoc)

diff --git a/sage-grep b/sage-grep
new file mode 100755
    - +  
     1#!/usr/bin/env bash 
     2 
     3cd $SAGE_ROOT/devel/sage/ 
     4 
     5find sage -print | egrep '.py([xdi])?$' | xargs grep "$@" 

  • new file sage-grepdoc 

    diff --git a/sage-grepdoc b/sage-grepdoc
new file mode 100755
    - +  
     1#!/usr/bin/env bash 
     2 
     3cd $SAGE_ROOT/devel/sage/doc/output 
     4 
     5find html -print | egrep '.html$' | xargs grep "$@"