mirror of
https://github.com/Mercury-Language/mercury.git
synced 2025-12-15 22:03:26 +00:00
b04f572e84
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.
4 lines
73 B
Plaintext
4 lines
73 B
Plaintext
dump $2 .mdb_grep_tmp
|
|
shell grep $1 .mdb_grep_tmp
|
|
shell rm .mdb_grep_tmp
|