package devkit

  1. Overview
  2. Docs
Development kit - general purpose library

Install

dune-project
 Dependency

Authors

Maintainers

Sources

1.20261006.tar.gz
md5=a39dbbce04bd5562a9b4443daf39c582
sha512=b10104b61384b2151521b785e7f3c3250134c75eae09b42cad69bc4a22a9a5e429beb891ee87cedf376c23d9c40f09d3f71c3fd48aa35df490c0f69dc17f3242

doc/devkit.core/Devkit_core/Action/class-timer_start/index.html

Class Action.timer_startSource

Basic timer. Also allows recording a sequence of interesting times from the given start point. Can serialize recorded events to json

method record : string -> Devkit_core.Time.t -> unit
method mark : string -> unit
method show : string
method json : (string * Yojson.Safe.t) list
method get : Devkit_core.Time.t
method get_str : string
method get_state : Devkit_core.Time.t * (string * Devkit_core.Time.t) list
method reset : unit

Resets both the internal start value, in addition to the list of recorded events