# HG changeset patch
# User lcp
# Date 788012786 -3600
# Node ID 8928f1c44d80e21d24898c0b80c351f76407a6c4
# Parent  0b9ec0374bfd61197462ff3ae93c8a9bbad8819d
Added comments and Id: marker.

diff -r 0b9ec0374bfd -r 8928f1c44d80 src/Tools/expandshort
--- a/src/Tools/expandshort	Wed Dec 21 13:10:39 1994 +0100
+++ b/src/Tools/expandshort	Wed Dec 21 13:26:26 1994 +0100
@@ -1,13 +1,13 @@
 #! /bin/sh
-#
-#expandshort - shell script to expand shorthand goal commands
+# $Id$
+#Shell script to expand shorthand goal commands
 #  ALSO contracts uses of resolve_tac, dresolve_tac, eresolve_tac,
 #     rewrite_goals_tac on 1-element lists
 #
 # Usage:
 #    expandshort FILE1 ... FILEn
 #
-#  leaves previous versions as XXX~~
+#Renames old versions of the files as FILE1~~ ... FILEn~~
 #
 for f in $*
 do