From f208fe7eb343486d3a464e0813d1cdce19b1ac5f Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 16 Dec 2006 18:59:48 +0000 Subject: [PATCH 1/1] Add rmuser command --- src/domain.sml | 2 +- src/main-admin.sml | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/domain.sml b/src/domain.sml index 04ee532..3d8290b 100644 --- a/src/domain.sml +++ b/src/domain.sml @@ -693,7 +693,7 @@ fun rmdom doms = before Posix.FileSys.closedir dir end handle OS.SysErr _ => - (print ("Warning: System error deleteing domain " ^ dom ^ " on " ^ node ^ ".\n"); + (print ("Warning: System error deleting domain " ^ dom ^ " on " ^ node ^ ".\n"); actions) in visitDom (dom, dname, actions) diff --git a/src/main-admin.sml b/src/main-admin.sml index 7305822..c36da01 100644 --- a/src/main-admin.sml +++ b/src/main-admin.sml @@ -43,4 +43,5 @@ val _ = print "\n")) | "rmdom" :: doms => Main.requestRmdom doms | ["regen"] => Main.requestRegen () + | ["rmuser", user] => Main.requestRmuser user | _ => print "Invalid command-line arguments\n" -- 2.20.1