aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/clib.mllib
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-07-29 14:34:41 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-07-29 14:34:41 +0200
commit8adafaf8c2f77c44b3202de8aea2bbb36acb0362 (patch)
tree1928dbaa48b586b83d20bf172db4a18134985803 /lib/clib.mllib
parent4580256452e3652df328d286b526c3c12dca7cae (diff)
Pp compiles after feedback
Diffstat (limited to 'lib/clib.mllib')
-rw-r--r--lib/clib.mllib2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 73839fd9e..160d49fba 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