A wrapper script for console.editfile().

584aabfe · rswindell · 510f4c70 · 584aabfe
Commit 584aabfe authored 5 years ago by rswindell
--- a/exec/editfile.js
+++ b/exec/editfile.js
+// $Id$
+
+if(argv[0])
+	console.editfile(argv[0]);
\ No newline at end of file