diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-17 11:01:32 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-17 11:34:51 +0100 |
| commit | 29f26d380177495a224c3b94d3309a3d23693d8f (patch) | |
| tree | 9cb911aae601214c0198b9becdce28b53315435c /lib | |
| parent | 6caf8b877e44862b21104236423c23972166cdd7 (diff) | |
Reducing the number of modules linked in grammar.cma.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/ppstyle.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/ppstyle.ml b/lib/ppstyle.ml index bb73fbdf5..3ecaac039 100644 --- a/lib/ppstyle.ml +++ b/lib/ppstyle.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util +module String = CString type t = string (** We use the concatenated string, with dots separating each string. We |