aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorBjoern B. Brandenburg <bbb@cs.unc.edu>2008-02-04 16:43:55 -0500
committerBjoern B. Brandenburg <bbb@cs.unc.edu>2008-02-04 16:43:55 -0500
commitf9d55f3a7930cd087554c33f355c79ff20c5d286 (patch)
treea22ac9d4512673b26f55747042be9d55eabacb2b
parentae57fe228629eff4dc9fce3fb4820da8ec6fde4f (diff)
add setsched tool
-rwxr-xr-xsetsched41
1 files changed, 41 insertions, 0 deletions
diff --git a/setsched b/setsched
new file mode 100755
index 0000000..411d999
--- /dev/null
+++ b/setsched
@@ -0,0 +1,41 @@
1#!/bin/bash
2#
3# setsched: facilitate changing the active scheduler plugin.
4
5ADIR=/proc/litmus/active_plugin
6PDIR=/proc/litmus/plugins
7
8CHOICE=$1
9
10if [ ! -e $ADIR ]; then
11 KERN=`uname -s -r`
12 echo "Error: LITMUS^RT not found on $KERN!"
13 exit 1
14fi
15
16ACTIVE=`cat $ADIR`
17
18if [ -z "$1" ]; then
19 TMP=`mktemp`
20 (awk "{print \$1 \" 'Plugin'\"}" $PDIR | \
21 xargs dialog --title "Select Plugin" --backtitle "Current: $ACTIVE" \
22 --cancel-label "Cancel" --ok-label "Select Plugin" \
23 --menu "Select a new plugin to run: " 23 60 16) 2> $TMP
24 OK=$?
25 clear
26 if [ "$OK" != "0" ]; then
27 exit 0;
28 fi
29 CHOICE=`cat $TMP`
30 rm $TMP
31fi
32
33
34echo "$CHOICE" > $ADIR
35
36ACTIVE=`cat $ADIR`
37
38if [ "$ACTIVE" != "$CHOICE" ]; then
39 echo "Error: Setting new plugin failed."
40 exit 1
41fi