Skip to content
This repository was archived by the owner on Aug 5, 2025. It is now read-only.
This repository was archived by the owner on Aug 5, 2025. It is now read-only.

Should the files matita/components/*/.depend[.opt] be under Git? #3

@fblanqui

Description

@fblanqui

Idem for ./matita/matita/.depend and ./elpi/bench/sources/lambdadelta/.depend:

15:57 ~/src/lpcic-matita-git find . -name .depend
./matita/components/extlib/.depend
./matita/components/content/.depend
./matita/components/ng_extraction/.depend
./matita/components/ng_cic_content/.depend
./matita/components/ng_refiner/.depend
./matita/components/grafite_engine/.depend
./matita/components/getter/.depend
./matita/components/ng_tactics/.depend
./matita/components/registry/.depend
./matita/components/xml/.depend
./matita/components/content_pres/.depend
./matita/components/ng_library/.depend
./matita/components/logger/.depend
./matita/components/thread/.depend
./matita/components/library/.depend
./matita/components/ng_disambiguation/.depend
./matita/components/disambiguation/.depend
./matita/components/grafite/.depend
./matita/components/syntax_extensions/.depend
./matita/components/ng_kernel/.depend
./matita/components/grafite_parser/.depend
./matita/components/ng_paramodulation/.depend
./matita/matita/.depend
./elpi/bench/sources/lambdadelta/.depend

Because, otherwise, after compilation, we get:

15:58 ~/src/lpcic-matita-git s
Sur la branche master
Votre branche est à jour avec 'origin/master'.
Modifications qui ne seront pas validées :
(utilisez "git add ..." pour mettre à jour ce qui sera validé)
(utilisez "git checkout -- ..." pour annuler les modifications dans la copie de travail)

modifié :         matita/components/content/.depend.opt
modifié :         matita/components/content_pres/.depend.opt
modifié :         matita/components/disambiguation/.depend.opt
modifié :         matita/components/extlib/.depend.opt
modifié :         matita/components/getter/.depend.opt
modifié :         matita/components/grafite/.depend.opt
modifié :         matita/components/grafite_engine/.depend.opt
modifié :         matita/components/grafite_parser/.depend.opt
modifié :         matita/components/library/.depend.opt
modifié :         matita/components/logger/.depend.opt
modifié :         matita/components/ng_cic_content/.depend.opt
modifié :         matita/components/ng_disambiguation/.depend.opt
modifié :         matita/components/ng_extraction/.depend.opt
modifié :         matita/components/ng_kernel/.depend.opt
modifié :         matita/components/ng_library/.depend.opt
modifié :         matita/components/ng_paramodulation/.depend.opt
modifié :         matita/components/ng_refiner/.depend.opt
modifié :         matita/components/ng_tactics/.depend.opt
modifié :         matita/components/registry/.depend.opt
modifié :         matita/components/syntax_extensions/.depend
modifié :         matita/components/syntax_extensions/.depend.opt
modifié :         matita/components/thread/.depend.opt
modifié :         matita/components/xml/.depend.opt
modifié :         matita/matita/.depend.opt

aucune modification n'a été ajoutée à la validation (utilisez "git add" ou "git commit -a")

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions