1 files changed, 8 insertions, 0 deletions
diff --git a/push.c b/push.c
index e5c940a..a725eb5 100644
--- a/push.c
+++ b/push.c
@@ -179,6 +179,14 @@ push_option (struct options *o, const char *opt, int msglevel)
 }
 
 void
+push_options (struct options *o, char **p, int msglevel, struct gc_arena *gc)
+{
+  const char **argv = make_extended_arg_array (p, gc);
+  char *opt = print_argv (argv, gc, 0);
+  push_option (o, opt, msglevel);
+}
+
+void
 push_reset (struct options *o)
 {
   o->push_list = NULL;