diff options
| author | pennae <github@quasiparticle.net> | 2023-06-23 00:26:52 +0200 |
|---|---|---|
| committer | pennae <github@quasiparticle.net> | 2023-07-01 20:59:30 +0200 |
| commit | f397309f4e6c7a219a7703b629f6a4e8d4e7a58b (patch) | |
| tree | 3e35e4bdd23c091c925f92e8fb227371559f8481 /doc/using | |
| parent | be4d19ff1a9a327ae805fdb344470ed6450256fc (diff) | |
doc: remove remnants of docbook times
all xml-related tooling can go away. shell.nix is no longer useful since
the makefile is gone and the build runs entirely via a derivation, and
gitignore is thus also no longer that useful. it may filter out some
swap files, but its main reason to exist (keeping generated files out of
a concurrent build of the derivation) has gone away.
Diffstat (limited to 'doc/using')
0 files changed, 0 insertions, 0 deletions