diff options
| author | Emilio Jesus Gallego Arias | 2019-07-10 16:07:09 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-23 18:53:46 +0200 |
| commit | bbf2ded61869b8aa48e34424c15e795961820721 (patch) | |
| tree | 4eee827763d4dfe7dee6dde0197cf1c865310f63 /dev/ci/ci-basic-overlay.sh | |
| parent | ae82afbaebb7f3a328498d4cc541d299423a7637 (diff) | |
[lemmas] Refactor code a bit, saving functions now to in the saving part.
We localize functions for constant saving that were used before in the
start hooks, but now they are called in the saving path in direct style.
No functional change.
Diffstat (limited to 'dev/ci/ci-basic-overlay.sh')
0 files changed, 0 insertions, 0 deletions