[m-rev.] diff: fix open and grep mdb scripts

[Ian MacLarty]

Estimated hours taken: 0.1
Branches: main

scripts/mdb_grep:
scripts/mdb_open:
	Replace "save_to_file" with "dump", since that mdb command has been
	renamed.

Index: scripts/mdb_grep
===================================================================
RCS file: /home/mercury1/repository/mercury/scripts/mdb_grep,v
retrieving revision 1.1
diff -u -r1.1 mdb_grep
--- scripts/mdb_grep	13 Jun 2006 09:49:00 -0000	1.1
+++ scripts/mdb_grep	25 Jul 2006 08:40:20 -0000
@@ -1,3 +1,3 @@
-save_to_file $2 .mdb_grep_tmp
+dump $2 .mdb_grep_tmp
 shell grep $1 .mdb_grep_tmp
 shell rm .mdb_grep_tmp
Index: scripts/mdb_open
===================================================================
RCS file: /home/mercury1/repository/mercury/scripts/mdb_open,v
retrieving revision 1.1
diff -u -r1.1 mdb_open
--- scripts/mdb_open	13 Jun 2006 09:49:00 -0000	1.1
+++ scripts/mdb_open	25 Jul 2006 08:40:10 -0000
@@ -1,3 +1,3 @@
-save_to_file $1 .mdb_open_tmp
+dump $1 .mdb_open_tmp
 shell ${EDITOR-vi} .mdb_open_tmp
 shell rm .mdb_open_tmp
--------------------------------------------------------------------------
mercury-reviews mailing list
Post messages to:       mercury-reviews at csse.unimelb.edu.au
Administrative Queries: owner-mercury-reviews at csse.unimelb.edu.au
Subscriptions:          mercury-reviews-request at csse.unimelb.edu.au
--------------------------------------------------------------------------