Admin/maketags
changeset 12721 226fc0e2e7e3
parent 9049 8a3101b62c4f
equal deleted inserted replaced
12720:f8a134b9a57f 12721:226fc0e2e7e3
     1 #!/bin/bash
     1 #!/usr/bin/env bash
     2 #
     2 #
     3 # $Id$
     3 # $Id$
     4 
     4 
     5 find . \( -name \*.ML -o -name \*.sml -o -name \*.sig \) -print | \
     5 find . \( -name \*.ML -o -name \*.sml -o -name \*.sig \) -print | \
     6   etags \
     6   etags \