diff options
Diffstat (limited to 'src/misc/mls.cil')
| -rw-r--r-- | src/misc/mls.cil | 11 |
1 files changed, 2 insertions, 9 deletions
diff --git a/src/misc/mls.cil b/src/misc/mls.cil index 357b4d0..007d757 100644 --- a/src/misc/mls.cil +++ b/src/misc/mls.cil @@ -1096,15 +1096,8 @@ c1011 c1012 c1013 c1014 c1015 c1016 c1017 c1018 c1019 c1020 c1021 c1022 c1023)) -(categoryset allcatset (range c0 c1023)) +(categoryset catset (range c0 c1023)) (sensitivity s0) (sensitivityorder (s0)) - -(sensitivitycategory s0 allcatset) - -(level systemlow (s0)) -(level systemhigh (s0 allcatset)) - -(levelrange lowlevelrange (systemlow systemlow)) -(levelrange lowhighlevelrange (systemlow systemhigh)) +(sensitivitycategory s0 catset) |