aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorEnrico Tassi2014-07-29 14:34:41 +0200
committerEnrico Tassi2014-07-29 14:34:41 +0200
commit8adafaf8c2f77c44b3202de8aea2bbb36acb0362 (patch)
tree1928dbaa48b586b83d20bf172db4a18134985803 /lib
parent4580256452e3652df328d286b526c3c12dca7cae (diff)
Pp compiles after feedback
Diffstat (limited to 'lib')
-rw-r--r--lib/clib.mllib2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 73839fd9e5..160d49fba9 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -19,7 +19,6 @@ Flags
Control
Loc
Serialize
-Pp
Deque
CObj
CList
@@ -29,6 +28,7 @@ CStack
Util
Stateid
Feedback
+Pp
CUnix
Envars
Aux_file