mainly new comments
This commit is contained in:
@@ -1,4 +1,9 @@
|
||||
DEFINITION MODULE Strings;
|
||||
(*
|
||||
Module: String manipulations
|
||||
Author: Ceriel J.H. Jacobs
|
||||
Version: $Header$
|
||||
*)
|
||||
(* Note: truncation of strings may occur if the user does not provide
|
||||
large enough variables to contain the result of the operation.
|
||||
*)
|
||||
|
||||
Reference in New Issue
Block a user